Proof of Theorem sspmlem
Step | Hyp | Ref
| Expression |
1 | | sspmlem.1 |
. . . . 5
⊢ (((𝑈 ∈ NrmCVec ∧ 𝑊 ∈ 𝐻) ∧ (𝑥 ∈ 𝑌 ∧ 𝑦 ∈ 𝑌)) → (𝑥𝐹𝑦) = (𝑥𝐺𝑦)) |
2 | | ovres 6800 |
. . . . . 6
⊢ ((𝑥 ∈ 𝑌 ∧ 𝑦 ∈ 𝑌) → (𝑥(𝐺 ↾ (𝑌 × 𝑌))𝑦) = (𝑥𝐺𝑦)) |
3 | 2 | adantl 482 |
. . . . 5
⊢ (((𝑈 ∈ NrmCVec ∧ 𝑊 ∈ 𝐻) ∧ (𝑥 ∈ 𝑌 ∧ 𝑦 ∈ 𝑌)) → (𝑥(𝐺 ↾ (𝑌 × 𝑌))𝑦) = (𝑥𝐺𝑦)) |
4 | 1, 3 | eqtr4d 2659 |
. . . 4
⊢ (((𝑈 ∈ NrmCVec ∧ 𝑊 ∈ 𝐻) ∧ (𝑥 ∈ 𝑌 ∧ 𝑦 ∈ 𝑌)) → (𝑥𝐹𝑦) = (𝑥(𝐺 ↾ (𝑌 × 𝑌))𝑦)) |
5 | 4 | ralrimivva 2971 |
. . 3
⊢ ((𝑈 ∈ NrmCVec ∧ 𝑊 ∈ 𝐻) → ∀𝑥 ∈ 𝑌 ∀𝑦 ∈ 𝑌 (𝑥𝐹𝑦) = (𝑥(𝐺 ↾ (𝑌 × 𝑌))𝑦)) |
6 | | eqid 2622 |
. . 3
⊢ (𝑌 × 𝑌) = (𝑌 × 𝑌) |
7 | 5, 6 | jctil 560 |
. 2
⊢ ((𝑈 ∈ NrmCVec ∧ 𝑊 ∈ 𝐻) → ((𝑌 × 𝑌) = (𝑌 × 𝑌) ∧ ∀𝑥 ∈ 𝑌 ∀𝑦 ∈ 𝑌 (𝑥𝐹𝑦) = (𝑥(𝐺 ↾ (𝑌 × 𝑌))𝑦))) |
8 | | sspmlem.h |
. . . . 5
⊢ 𝐻 = (SubSp‘𝑈) |
9 | 8 | sspnv 27581 |
. . . 4
⊢ ((𝑈 ∈ NrmCVec ∧ 𝑊 ∈ 𝐻) → 𝑊 ∈ NrmCVec) |
10 | | sspmlem.2 |
. . . 4
⊢ (𝑊 ∈ NrmCVec → 𝐹:(𝑌 × 𝑌)⟶𝑅) |
11 | | ffn 6045 |
. . . 4
⊢ (𝐹:(𝑌 × 𝑌)⟶𝑅 → 𝐹 Fn (𝑌 × 𝑌)) |
12 | 9, 10, 11 | 3syl 18 |
. . 3
⊢ ((𝑈 ∈ NrmCVec ∧ 𝑊 ∈ 𝐻) → 𝐹 Fn (𝑌 × 𝑌)) |
13 | | sspmlem.3 |
. . . . . 6
⊢ (𝑈 ∈ NrmCVec → 𝐺:((BaseSet‘𝑈) × (BaseSet‘𝑈))⟶𝑆) |
14 | | ffn 6045 |
. . . . . 6
⊢ (𝐺:((BaseSet‘𝑈) × (BaseSet‘𝑈))⟶𝑆 → 𝐺 Fn ((BaseSet‘𝑈) × (BaseSet‘𝑈))) |
15 | 13, 14 | syl 17 |
. . . . 5
⊢ (𝑈 ∈ NrmCVec → 𝐺 Fn ((BaseSet‘𝑈) × (BaseSet‘𝑈))) |
16 | 15 | adantr 481 |
. . . 4
⊢ ((𝑈 ∈ NrmCVec ∧ 𝑊 ∈ 𝐻) → 𝐺 Fn ((BaseSet‘𝑈) × (BaseSet‘𝑈))) |
17 | | eqid 2622 |
. . . . . 6
⊢
(BaseSet‘𝑈) =
(BaseSet‘𝑈) |
18 | | sspmlem.y |
. . . . . 6
⊢ 𝑌 = (BaseSet‘𝑊) |
19 | 17, 18, 8 | sspba 27582 |
. . . . 5
⊢ ((𝑈 ∈ NrmCVec ∧ 𝑊 ∈ 𝐻) → 𝑌 ⊆ (BaseSet‘𝑈)) |
20 | | xpss12 5225 |
. . . . 5
⊢ ((𝑌 ⊆ (BaseSet‘𝑈) ∧ 𝑌 ⊆ (BaseSet‘𝑈)) → (𝑌 × 𝑌) ⊆ ((BaseSet‘𝑈) × (BaseSet‘𝑈))) |
21 | 19, 19, 20 | syl2anc 693 |
. . . 4
⊢ ((𝑈 ∈ NrmCVec ∧ 𝑊 ∈ 𝐻) → (𝑌 × 𝑌) ⊆ ((BaseSet‘𝑈) × (BaseSet‘𝑈))) |
22 | | fnssres 6004 |
. . . 4
⊢ ((𝐺 Fn ((BaseSet‘𝑈) × (BaseSet‘𝑈)) ∧ (𝑌 × 𝑌) ⊆ ((BaseSet‘𝑈) × (BaseSet‘𝑈))) → (𝐺 ↾ (𝑌 × 𝑌)) Fn (𝑌 × 𝑌)) |
23 | 16, 21, 22 | syl2anc 693 |
. . 3
⊢ ((𝑈 ∈ NrmCVec ∧ 𝑊 ∈ 𝐻) → (𝐺 ↾ (𝑌 × 𝑌)) Fn (𝑌 × 𝑌)) |
24 | | eqfnov 6766 |
. . 3
⊢ ((𝐹 Fn (𝑌 × 𝑌) ∧ (𝐺 ↾ (𝑌 × 𝑌)) Fn (𝑌 × 𝑌)) → (𝐹 = (𝐺 ↾ (𝑌 × 𝑌)) ↔ ((𝑌 × 𝑌) = (𝑌 × 𝑌) ∧ ∀𝑥 ∈ 𝑌 ∀𝑦 ∈ 𝑌 (𝑥𝐹𝑦) = (𝑥(𝐺 ↾ (𝑌 × 𝑌))𝑦)))) |
25 | 12, 23, 24 | syl2anc 693 |
. 2
⊢ ((𝑈 ∈ NrmCVec ∧ 𝑊 ∈ 𝐻) → (𝐹 = (𝐺 ↾ (𝑌 × 𝑌)) ↔ ((𝑌 × 𝑌) = (𝑌 × 𝑌) ∧ ∀𝑥 ∈ 𝑌 ∀𝑦 ∈ 𝑌 (𝑥𝐹𝑦) = (𝑥(𝐺 ↾ (𝑌 × 𝑌))𝑦)))) |
26 | 7, 25 | mpbird 247 |
1
⊢ ((𝑈 ∈ NrmCVec ∧ 𝑊 ∈ 𝐻) → 𝐹 = (𝐺 ↾ (𝑌 × 𝑌))) |