Step | Hyp | Ref
| Expression |
1 | | diblsmopel.k |
. . 3
⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻)) |
2 | | diblsmopel.x |
. . . 4
⊢ (𝜑 → (𝑋 ∈ 𝐵 ∧ 𝑋 ≤ 𝑊)) |
3 | | diblsmopel.b |
. . . . 5
⊢ 𝐵 = (Base‘𝐾) |
4 | | diblsmopel.l |
. . . . 5
⊢ ≤ =
(le‘𝐾) |
5 | | diblsmopel.h |
. . . . 5
⊢ 𝐻 = (LHyp‘𝐾) |
6 | | diblsmopel.u |
. . . . 5
⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊) |
7 | | diblsmopel.i |
. . . . 5
⊢ 𝐼 = ((DIsoB‘𝐾)‘𝑊) |
8 | | eqid 2610 |
. . . . 5
⊢
(LSubSp‘𝑈) =
(LSubSp‘𝑈) |
9 | 3, 4, 5, 6, 7, 8 | diblss 35477 |
. . . 4
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ 𝑋 ≤ 𝑊)) → (𝐼‘𝑋) ∈ (LSubSp‘𝑈)) |
10 | 1, 2, 9 | syl2anc 691 |
. . 3
⊢ (𝜑 → (𝐼‘𝑋) ∈ (LSubSp‘𝑈)) |
11 | | diblsmopel.y |
. . . 4
⊢ (𝜑 → (𝑌 ∈ 𝐵 ∧ 𝑌 ≤ 𝑊)) |
12 | 3, 4, 5, 6, 7, 8 | diblss 35477 |
. . . 4
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑌 ∈ 𝐵 ∧ 𝑌 ≤ 𝑊)) → (𝐼‘𝑌) ∈ (LSubSp‘𝑈)) |
13 | 1, 11, 12 | syl2anc 691 |
. . 3
⊢ (𝜑 → (𝐼‘𝑌) ∈ (LSubSp‘𝑈)) |
14 | | eqid 2610 |
. . . 4
⊢
(+g‘𝑈) = (+g‘𝑈) |
15 | | diblsmopel.p |
. . . 4
⊢ ✚ =
(LSSum‘𝑈) |
16 | 5, 6, 14, 8, 15 | dvhopellsm 35424 |
. . 3
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐼‘𝑋) ∈ (LSubSp‘𝑈) ∧ (𝐼‘𝑌) ∈ (LSubSp‘𝑈)) → (〈𝐹, 𝑆〉 ∈ ((𝐼‘𝑋) ✚ (𝐼‘𝑌)) ↔ ∃𝑥∃𝑦∃𝑧∃𝑤((〈𝑥, 𝑦〉 ∈ (𝐼‘𝑋) ∧ 〈𝑧, 𝑤〉 ∈ (𝐼‘𝑌)) ∧ 〈𝐹, 𝑆〉 = (〈𝑥, 𝑦〉(+g‘𝑈)〈𝑧, 𝑤〉)))) |
17 | 1, 10, 13, 16 | syl3anc 1318 |
. 2
⊢ (𝜑 → (〈𝐹, 𝑆〉 ∈ ((𝐼‘𝑋) ✚ (𝐼‘𝑌)) ↔ ∃𝑥∃𝑦∃𝑧∃𝑤((〈𝑥, 𝑦〉 ∈ (𝐼‘𝑋) ∧ 〈𝑧, 𝑤〉 ∈ (𝐼‘𝑌)) ∧ 〈𝐹, 𝑆〉 = (〈𝑥, 𝑦〉(+g‘𝑈)〈𝑧, 𝑤〉)))) |
18 | | excom 2029 |
. . . 4
⊢
(∃𝑦∃𝑧∃𝑤((〈𝑥, 𝑦〉 ∈ (𝐼‘𝑋) ∧ 〈𝑧, 𝑤〉 ∈ (𝐼‘𝑌)) ∧ 〈𝐹, 𝑆〉 = (〈𝑥, 𝑦〉(+g‘𝑈)〈𝑧, 𝑤〉)) ↔ ∃𝑧∃𝑦∃𝑤((〈𝑥, 𝑦〉 ∈ (𝐼‘𝑋) ∧ 〈𝑧, 𝑤〉 ∈ (𝐼‘𝑌)) ∧ 〈𝐹, 𝑆〉 = (〈𝑥, 𝑦〉(+g‘𝑈)〈𝑧, 𝑤〉))) |
19 | | diblsmopel.t |
. . . . . . . . . . . . 13
⊢ 𝑇 = ((LTrn‘𝐾)‘𝑊) |
20 | | diblsmopel.o |
. . . . . . . . . . . . 13
⊢ 𝑂 = (𝑓 ∈ 𝑇 ↦ ( I ↾ 𝐵)) |
21 | | diblsmopel.j |
. . . . . . . . . . . . 13
⊢ 𝐽 = ((DIsoA‘𝐾)‘𝑊) |
22 | 3, 4, 5, 19, 20, 21, 7 | dibopelval2 35452 |
. . . . . . . . . . . 12
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ 𝑋 ≤ 𝑊)) → (〈𝑥, 𝑦〉 ∈ (𝐼‘𝑋) ↔ (𝑥 ∈ (𝐽‘𝑋) ∧ 𝑦 = 𝑂))) |
23 | 1, 2, 22 | syl2anc 691 |
. . . . . . . . . . 11
⊢ (𝜑 → (〈𝑥, 𝑦〉 ∈ (𝐼‘𝑋) ↔ (𝑥 ∈ (𝐽‘𝑋) ∧ 𝑦 = 𝑂))) |
24 | 3, 4, 5, 19, 20, 21, 7 | dibopelval2 35452 |
. . . . . . . . . . . 12
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑌 ∈ 𝐵 ∧ 𝑌 ≤ 𝑊)) → (〈𝑧, 𝑤〉 ∈ (𝐼‘𝑌) ↔ (𝑧 ∈ (𝐽‘𝑌) ∧ 𝑤 = 𝑂))) |
25 | 1, 11, 24 | syl2anc 691 |
. . . . . . . . . . 11
⊢ (𝜑 → (〈𝑧, 𝑤〉 ∈ (𝐼‘𝑌) ↔ (𝑧 ∈ (𝐽‘𝑌) ∧ 𝑤 = 𝑂))) |
26 | 23, 25 | anbi12d 743 |
. . . . . . . . . 10
⊢ (𝜑 → ((〈𝑥, 𝑦〉 ∈ (𝐼‘𝑋) ∧ 〈𝑧, 𝑤〉 ∈ (𝐼‘𝑌)) ↔ ((𝑥 ∈ (𝐽‘𝑋) ∧ 𝑦 = 𝑂) ∧ (𝑧 ∈ (𝐽‘𝑌) ∧ 𝑤 = 𝑂)))) |
27 | | an4 861 |
. . . . . . . . . . 11
⊢ (((𝑥 ∈ (𝐽‘𝑋) ∧ 𝑦 = 𝑂) ∧ (𝑧 ∈ (𝐽‘𝑌) ∧ 𝑤 = 𝑂)) ↔ ((𝑥 ∈ (𝐽‘𝑋) ∧ 𝑧 ∈ (𝐽‘𝑌)) ∧ (𝑦 = 𝑂 ∧ 𝑤 = 𝑂))) |
28 | | ancom 465 |
. . . . . . . . . . 11
⊢ (((𝑥 ∈ (𝐽‘𝑋) ∧ 𝑧 ∈ (𝐽‘𝑌)) ∧ (𝑦 = 𝑂 ∧ 𝑤 = 𝑂)) ↔ ((𝑦 = 𝑂 ∧ 𝑤 = 𝑂) ∧ (𝑥 ∈ (𝐽‘𝑋) ∧ 𝑧 ∈ (𝐽‘𝑌)))) |
29 | 27, 28 | bitri 263 |
. . . . . . . . . 10
⊢ (((𝑥 ∈ (𝐽‘𝑋) ∧ 𝑦 = 𝑂) ∧ (𝑧 ∈ (𝐽‘𝑌) ∧ 𝑤 = 𝑂)) ↔ ((𝑦 = 𝑂 ∧ 𝑤 = 𝑂) ∧ (𝑥 ∈ (𝐽‘𝑋) ∧ 𝑧 ∈ (𝐽‘𝑌)))) |
30 | 26, 29 | syl6bb 275 |
. . . . . . . . 9
⊢ (𝜑 → ((〈𝑥, 𝑦〉 ∈ (𝐼‘𝑋) ∧ 〈𝑧, 𝑤〉 ∈ (𝐼‘𝑌)) ↔ ((𝑦 = 𝑂 ∧ 𝑤 = 𝑂) ∧ (𝑥 ∈ (𝐽‘𝑋) ∧ 𝑧 ∈ (𝐽‘𝑌))))) |
31 | 30 | anbi1d 737 |
. . . . . . . 8
⊢ (𝜑 → (((〈𝑥, 𝑦〉 ∈ (𝐼‘𝑋) ∧ 〈𝑧, 𝑤〉 ∈ (𝐼‘𝑌)) ∧ 〈𝐹, 𝑆〉 = (〈𝑥, 𝑦〉(+g‘𝑈)〈𝑧, 𝑤〉)) ↔ (((𝑦 = 𝑂 ∧ 𝑤 = 𝑂) ∧ (𝑥 ∈ (𝐽‘𝑋) ∧ 𝑧 ∈ (𝐽‘𝑌))) ∧ 〈𝐹, 𝑆〉 = (〈𝑥, 𝑦〉(+g‘𝑈)〈𝑧, 𝑤〉)))) |
32 | | anass 679 |
. . . . . . . . 9
⊢ ((((𝑦 = 𝑂 ∧ 𝑤 = 𝑂) ∧ (𝑥 ∈ (𝐽‘𝑋) ∧ 𝑧 ∈ (𝐽‘𝑌))) ∧ 〈𝐹, 𝑆〉 = (〈𝑥, 𝑦〉(+g‘𝑈)〈𝑧, 𝑤〉)) ↔ ((𝑦 = 𝑂 ∧ 𝑤 = 𝑂) ∧ ((𝑥 ∈ (𝐽‘𝑋) ∧ 𝑧 ∈ (𝐽‘𝑌)) ∧ 〈𝐹, 𝑆〉 = (〈𝑥, 𝑦〉(+g‘𝑈)〈𝑧, 𝑤〉)))) |
33 | | df-3an 1033 |
. . . . . . . . 9
⊢ ((𝑦 = 𝑂 ∧ 𝑤 = 𝑂 ∧ ((𝑥 ∈ (𝐽‘𝑋) ∧ 𝑧 ∈ (𝐽‘𝑌)) ∧ 〈𝐹, 𝑆〉 = (〈𝑥, 𝑦〉(+g‘𝑈)〈𝑧, 𝑤〉))) ↔ ((𝑦 = 𝑂 ∧ 𝑤 = 𝑂) ∧ ((𝑥 ∈ (𝐽‘𝑋) ∧ 𝑧 ∈ (𝐽‘𝑌)) ∧ 〈𝐹, 𝑆〉 = (〈𝑥, 𝑦〉(+g‘𝑈)〈𝑧, 𝑤〉)))) |
34 | 32, 33 | bitr4i 266 |
. . . . . . . 8
⊢ ((((𝑦 = 𝑂 ∧ 𝑤 = 𝑂) ∧ (𝑥 ∈ (𝐽‘𝑋) ∧ 𝑧 ∈ (𝐽‘𝑌))) ∧ 〈𝐹, 𝑆〉 = (〈𝑥, 𝑦〉(+g‘𝑈)〈𝑧, 𝑤〉)) ↔ (𝑦 = 𝑂 ∧ 𝑤 = 𝑂 ∧ ((𝑥 ∈ (𝐽‘𝑋) ∧ 𝑧 ∈ (𝐽‘𝑌)) ∧ 〈𝐹, 𝑆〉 = (〈𝑥, 𝑦〉(+g‘𝑈)〈𝑧, 𝑤〉)))) |
35 | 31, 34 | syl6bb 275 |
. . . . . . 7
⊢ (𝜑 → (((〈𝑥, 𝑦〉 ∈ (𝐼‘𝑋) ∧ 〈𝑧, 𝑤〉 ∈ (𝐼‘𝑌)) ∧ 〈𝐹, 𝑆〉 = (〈𝑥, 𝑦〉(+g‘𝑈)〈𝑧, 𝑤〉)) ↔ (𝑦 = 𝑂 ∧ 𝑤 = 𝑂 ∧ ((𝑥 ∈ (𝐽‘𝑋) ∧ 𝑧 ∈ (𝐽‘𝑌)) ∧ 〈𝐹, 𝑆〉 = (〈𝑥, 𝑦〉(+g‘𝑈)〈𝑧, 𝑤〉))))) |
36 | 35 | 2exbidv 1839 |
. . . . . 6
⊢ (𝜑 → (∃𝑦∃𝑤((〈𝑥, 𝑦〉 ∈ (𝐼‘𝑋) ∧ 〈𝑧, 𝑤〉 ∈ (𝐼‘𝑌)) ∧ 〈𝐹, 𝑆〉 = (〈𝑥, 𝑦〉(+g‘𝑈)〈𝑧, 𝑤〉)) ↔ ∃𝑦∃𝑤(𝑦 = 𝑂 ∧ 𝑤 = 𝑂 ∧ ((𝑥 ∈ (𝐽‘𝑋) ∧ 𝑧 ∈ (𝐽‘𝑌)) ∧ 〈𝐹, 𝑆〉 = (〈𝑥, 𝑦〉(+g‘𝑈)〈𝑧, 𝑤〉))))) |
37 | | fvex 6113 |
. . . . . . . . . . 11
⊢
((LTrn‘𝐾)‘𝑊) ∈ V |
38 | 19, 37 | eqeltri 2684 |
. . . . . . . . . 10
⊢ 𝑇 ∈ V |
39 | 38 | mptex 6390 |
. . . . . . . . 9
⊢ (𝑓 ∈ 𝑇 ↦ ( I ↾ 𝐵)) ∈ V |
40 | 20, 39 | eqeltri 2684 |
. . . . . . . 8
⊢ 𝑂 ∈ V |
41 | | opeq2 4341 |
. . . . . . . . . . 11
⊢ (𝑦 = 𝑂 → 〈𝑥, 𝑦〉 = 〈𝑥, 𝑂〉) |
42 | 41 | oveq1d 6564 |
. . . . . . . . . 10
⊢ (𝑦 = 𝑂 → (〈𝑥, 𝑦〉(+g‘𝑈)〈𝑧, 𝑤〉) = (〈𝑥, 𝑂〉(+g‘𝑈)〈𝑧, 𝑤〉)) |
43 | 42 | eqeq2d 2620 |
. . . . . . . . 9
⊢ (𝑦 = 𝑂 → (〈𝐹, 𝑆〉 = (〈𝑥, 𝑦〉(+g‘𝑈)〈𝑧, 𝑤〉) ↔ 〈𝐹, 𝑆〉 = (〈𝑥, 𝑂〉(+g‘𝑈)〈𝑧, 𝑤〉))) |
44 | 43 | anbi2d 736 |
. . . . . . . 8
⊢ (𝑦 = 𝑂 → (((𝑥 ∈ (𝐽‘𝑋) ∧ 𝑧 ∈ (𝐽‘𝑌)) ∧ 〈𝐹, 𝑆〉 = (〈𝑥, 𝑦〉(+g‘𝑈)〈𝑧, 𝑤〉)) ↔ ((𝑥 ∈ (𝐽‘𝑋) ∧ 𝑧 ∈ (𝐽‘𝑌)) ∧ 〈𝐹, 𝑆〉 = (〈𝑥, 𝑂〉(+g‘𝑈)〈𝑧, 𝑤〉)))) |
45 | | opeq2 4341 |
. . . . . . . . . . 11
⊢ (𝑤 = 𝑂 → 〈𝑧, 𝑤〉 = 〈𝑧, 𝑂〉) |
46 | 45 | oveq2d 6565 |
. . . . . . . . . 10
⊢ (𝑤 = 𝑂 → (〈𝑥, 𝑂〉(+g‘𝑈)〈𝑧, 𝑤〉) = (〈𝑥, 𝑂〉(+g‘𝑈)〈𝑧, 𝑂〉)) |
47 | 46 | eqeq2d 2620 |
. . . . . . . . 9
⊢ (𝑤 = 𝑂 → (〈𝐹, 𝑆〉 = (〈𝑥, 𝑂〉(+g‘𝑈)〈𝑧, 𝑤〉) ↔ 〈𝐹, 𝑆〉 = (〈𝑥, 𝑂〉(+g‘𝑈)〈𝑧, 𝑂〉))) |
48 | 47 | anbi2d 736 |
. . . . . . . 8
⊢ (𝑤 = 𝑂 → (((𝑥 ∈ (𝐽‘𝑋) ∧ 𝑧 ∈ (𝐽‘𝑌)) ∧ 〈𝐹, 𝑆〉 = (〈𝑥, 𝑂〉(+g‘𝑈)〈𝑧, 𝑤〉)) ↔ ((𝑥 ∈ (𝐽‘𝑋) ∧ 𝑧 ∈ (𝐽‘𝑌)) ∧ 〈𝐹, 𝑆〉 = (〈𝑥, 𝑂〉(+g‘𝑈)〈𝑧, 𝑂〉)))) |
49 | 40, 40, 44, 48 | ceqsex2v 3218 |
. . . . . . 7
⊢
(∃𝑦∃𝑤(𝑦 = 𝑂 ∧ 𝑤 = 𝑂 ∧ ((𝑥 ∈ (𝐽‘𝑋) ∧ 𝑧 ∈ (𝐽‘𝑌)) ∧ 〈𝐹, 𝑆〉 = (〈𝑥, 𝑦〉(+g‘𝑈)〈𝑧, 𝑤〉))) ↔ ((𝑥 ∈ (𝐽‘𝑋) ∧ 𝑧 ∈ (𝐽‘𝑌)) ∧ 〈𝐹, 𝑆〉 = (〈𝑥, 𝑂〉(+g‘𝑈)〈𝑧, 𝑂〉))) |
50 | 1 | adantr 480 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑥 ∈ (𝐽‘𝑋) ∧ 𝑧 ∈ (𝐽‘𝑌))) → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻)) |
51 | 2 | adantr 480 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑥 ∈ (𝐽‘𝑋) ∧ 𝑧 ∈ (𝐽‘𝑌))) → (𝑋 ∈ 𝐵 ∧ 𝑋 ≤ 𝑊)) |
52 | | simprl 790 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑥 ∈ (𝐽‘𝑋) ∧ 𝑧 ∈ (𝐽‘𝑌))) → 𝑥 ∈ (𝐽‘𝑋)) |
53 | 3, 4, 5, 19, 21 | diael 35350 |
. . . . . . . . . . . 12
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ 𝑋 ≤ 𝑊) ∧ 𝑥 ∈ (𝐽‘𝑋)) → 𝑥 ∈ 𝑇) |
54 | 50, 51, 52, 53 | syl3anc 1318 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑥 ∈ (𝐽‘𝑋) ∧ 𝑧 ∈ (𝐽‘𝑌))) → 𝑥 ∈ 𝑇) |
55 | | eqid 2610 |
. . . . . . . . . . . . 13
⊢
((TEndo‘𝐾)‘𝑊) = ((TEndo‘𝐾)‘𝑊) |
56 | 3, 5, 19, 55, 20 | tendo0cl 35096 |
. . . . . . . . . . . 12
⊢ ((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) → 𝑂 ∈ ((TEndo‘𝐾)‘𝑊)) |
57 | 50, 56 | syl 17 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑥 ∈ (𝐽‘𝑋) ∧ 𝑧 ∈ (𝐽‘𝑌))) → 𝑂 ∈ ((TEndo‘𝐾)‘𝑊)) |
58 | 11 | adantr 480 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑥 ∈ (𝐽‘𝑋) ∧ 𝑧 ∈ (𝐽‘𝑌))) → (𝑌 ∈ 𝐵 ∧ 𝑌 ≤ 𝑊)) |
59 | | simprr 792 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑥 ∈ (𝐽‘𝑋) ∧ 𝑧 ∈ (𝐽‘𝑌))) → 𝑧 ∈ (𝐽‘𝑌)) |
60 | 3, 4, 5, 19, 21 | diael 35350 |
. . . . . . . . . . . 12
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑌 ∈ 𝐵 ∧ 𝑌 ≤ 𝑊) ∧ 𝑧 ∈ (𝐽‘𝑌)) → 𝑧 ∈ 𝑇) |
61 | 50, 58, 59, 60 | syl3anc 1318 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑥 ∈ (𝐽‘𝑋) ∧ 𝑧 ∈ (𝐽‘𝑌))) → 𝑧 ∈ 𝑇) |
62 | | eqid 2610 |
. . . . . . . . . . . 12
⊢
(Scalar‘𝑈) =
(Scalar‘𝑈) |
63 | | eqid 2610 |
. . . . . . . . . . . 12
⊢
(+g‘(Scalar‘𝑈)) =
(+g‘(Scalar‘𝑈)) |
64 | 5, 19, 55, 6, 62, 14, 63 | dvhopvadd 35400 |
. . . . . . . . . . 11
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑥 ∈ 𝑇 ∧ 𝑂 ∈ ((TEndo‘𝐾)‘𝑊)) ∧ (𝑧 ∈ 𝑇 ∧ 𝑂 ∈ ((TEndo‘𝐾)‘𝑊))) → (〈𝑥, 𝑂〉(+g‘𝑈)〈𝑧, 𝑂〉) = 〈(𝑥 ∘ 𝑧), (𝑂(+g‘(Scalar‘𝑈))𝑂)〉) |
65 | 50, 54, 57, 61, 57, 64 | syl122anc 1327 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑥 ∈ (𝐽‘𝑋) ∧ 𝑧 ∈ (𝐽‘𝑌))) → (〈𝑥, 𝑂〉(+g‘𝑈)〈𝑧, 𝑂〉) = 〈(𝑥 ∘ 𝑧), (𝑂(+g‘(Scalar‘𝑈))𝑂)〉) |
66 | 65 | eqeq2d 2620 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑥 ∈ (𝐽‘𝑋) ∧ 𝑧 ∈ (𝐽‘𝑌))) → (〈𝐹, 𝑆〉 = (〈𝑥, 𝑂〉(+g‘𝑈)〈𝑧, 𝑂〉) ↔ 〈𝐹, 𝑆〉 = 〈(𝑥 ∘ 𝑧), (𝑂(+g‘(Scalar‘𝑈))𝑂)〉)) |
67 | | vex 3176 |
. . . . . . . . . . . 12
⊢ 𝑥 ∈ V |
68 | | vex 3176 |
. . . . . . . . . . . 12
⊢ 𝑧 ∈ V |
69 | 67, 68 | coex 7011 |
. . . . . . . . . . 11
⊢ (𝑥 ∘ 𝑧) ∈ V |
70 | | ovex 6577 |
. . . . . . . . . . 11
⊢ (𝑂(+g‘(Scalar‘𝑈))𝑂) ∈ V |
71 | 69, 70 | opth2 4875 |
. . . . . . . . . 10
⊢
(〈𝐹, 𝑆〉 = 〈(𝑥 ∘ 𝑧), (𝑂(+g‘(Scalar‘𝑈))𝑂)〉 ↔ (𝐹 = (𝑥 ∘ 𝑧) ∧ 𝑆 = (𝑂(+g‘(Scalar‘𝑈))𝑂))) |
72 | | diblsmopel.v |
. . . . . . . . . . . . . . 15
⊢ 𝑉 = ((DVecA‘𝐾)‘𝑊) |
73 | | eqid 2610 |
. . . . . . . . . . . . . . 15
⊢
(+g‘𝑉) = (+g‘𝑉) |
74 | 5, 19, 72, 73 | dvavadd 35321 |
. . . . . . . . . . . . . 14
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑥 ∈ 𝑇 ∧ 𝑧 ∈ 𝑇)) → (𝑥(+g‘𝑉)𝑧) = (𝑥 ∘ 𝑧)) |
75 | 50, 54, 61, 74 | syl12anc 1316 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ (𝑥 ∈ (𝐽‘𝑋) ∧ 𝑧 ∈ (𝐽‘𝑌))) → (𝑥(+g‘𝑉)𝑧) = (𝑥 ∘ 𝑧)) |
76 | 75 | eqeq2d 2620 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑥 ∈ (𝐽‘𝑋) ∧ 𝑧 ∈ (𝐽‘𝑌))) → (𝐹 = (𝑥(+g‘𝑉)𝑧) ↔ 𝐹 = (𝑥 ∘ 𝑧))) |
77 | 76 | bicomd 212 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑥 ∈ (𝐽‘𝑋) ∧ 𝑧 ∈ (𝐽‘𝑌))) → (𝐹 = (𝑥 ∘ 𝑧) ↔ 𝐹 = (𝑥(+g‘𝑉)𝑧))) |
78 | | eqid 2610 |
. . . . . . . . . . . . . . . 16
⊢ (𝑠 ∈ ((TEndo‘𝐾)‘𝑊), 𝑡 ∈ ((TEndo‘𝐾)‘𝑊) ↦ (𝑓 ∈ 𝑇 ↦ ((𝑠‘𝑓) ∘ (𝑡‘𝑓)))) = (𝑠 ∈ ((TEndo‘𝐾)‘𝑊), 𝑡 ∈ ((TEndo‘𝐾)‘𝑊) ↦ (𝑓 ∈ 𝑇 ↦ ((𝑠‘𝑓) ∘ (𝑡‘𝑓)))) |
79 | 5, 19, 55, 6, 62, 78, 63 | dvhfplusr 35391 |
. . . . . . . . . . . . . . 15
⊢ ((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) →
(+g‘(Scalar‘𝑈)) = (𝑠 ∈ ((TEndo‘𝐾)‘𝑊), 𝑡 ∈ ((TEndo‘𝐾)‘𝑊) ↦ (𝑓 ∈ 𝑇 ↦ ((𝑠‘𝑓) ∘ (𝑡‘𝑓))))) |
80 | 50, 79 | syl 17 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ (𝑥 ∈ (𝐽‘𝑋) ∧ 𝑧 ∈ (𝐽‘𝑌))) →
(+g‘(Scalar‘𝑈)) = (𝑠 ∈ ((TEndo‘𝐾)‘𝑊), 𝑡 ∈ ((TEndo‘𝐾)‘𝑊) ↦ (𝑓 ∈ 𝑇 ↦ ((𝑠‘𝑓) ∘ (𝑡‘𝑓))))) |
81 | 80 | oveqd 6566 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ (𝑥 ∈ (𝐽‘𝑋) ∧ 𝑧 ∈ (𝐽‘𝑌))) → (𝑂(+g‘(Scalar‘𝑈))𝑂) = (𝑂(𝑠 ∈ ((TEndo‘𝐾)‘𝑊), 𝑡 ∈ ((TEndo‘𝐾)‘𝑊) ↦ (𝑓 ∈ 𝑇 ↦ ((𝑠‘𝑓) ∘ (𝑡‘𝑓))))𝑂)) |
82 | 3, 5, 19, 55, 20, 78 | tendo0pl 35097 |
. . . . . . . . . . . . . 14
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑂 ∈ ((TEndo‘𝐾)‘𝑊)) → (𝑂(𝑠 ∈ ((TEndo‘𝐾)‘𝑊), 𝑡 ∈ ((TEndo‘𝐾)‘𝑊) ↦ (𝑓 ∈ 𝑇 ↦ ((𝑠‘𝑓) ∘ (𝑡‘𝑓))))𝑂) = 𝑂) |
83 | 50, 57, 82 | syl2anc 691 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ (𝑥 ∈ (𝐽‘𝑋) ∧ 𝑧 ∈ (𝐽‘𝑌))) → (𝑂(𝑠 ∈ ((TEndo‘𝐾)‘𝑊), 𝑡 ∈ ((TEndo‘𝐾)‘𝑊) ↦ (𝑓 ∈ 𝑇 ↦ ((𝑠‘𝑓) ∘ (𝑡‘𝑓))))𝑂) = 𝑂) |
84 | 81, 83 | eqtrd 2644 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑥 ∈ (𝐽‘𝑋) ∧ 𝑧 ∈ (𝐽‘𝑌))) → (𝑂(+g‘(Scalar‘𝑈))𝑂) = 𝑂) |
85 | 84 | eqeq2d 2620 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑥 ∈ (𝐽‘𝑋) ∧ 𝑧 ∈ (𝐽‘𝑌))) → (𝑆 = (𝑂(+g‘(Scalar‘𝑈))𝑂) ↔ 𝑆 = 𝑂)) |
86 | 77, 85 | anbi12d 743 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑥 ∈ (𝐽‘𝑋) ∧ 𝑧 ∈ (𝐽‘𝑌))) → ((𝐹 = (𝑥 ∘ 𝑧) ∧ 𝑆 = (𝑂(+g‘(Scalar‘𝑈))𝑂)) ↔ (𝐹 = (𝑥(+g‘𝑉)𝑧) ∧ 𝑆 = 𝑂))) |
87 | 71, 86 | syl5bb 271 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑥 ∈ (𝐽‘𝑋) ∧ 𝑧 ∈ (𝐽‘𝑌))) → (〈𝐹, 𝑆〉 = 〈(𝑥 ∘ 𝑧), (𝑂(+g‘(Scalar‘𝑈))𝑂)〉 ↔ (𝐹 = (𝑥(+g‘𝑉)𝑧) ∧ 𝑆 = 𝑂))) |
88 | 66, 87 | bitrd 267 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑥 ∈ (𝐽‘𝑋) ∧ 𝑧 ∈ (𝐽‘𝑌))) → (〈𝐹, 𝑆〉 = (〈𝑥, 𝑂〉(+g‘𝑈)〈𝑧, 𝑂〉) ↔ (𝐹 = (𝑥(+g‘𝑉)𝑧) ∧ 𝑆 = 𝑂))) |
89 | 88 | pm5.32da 671 |
. . . . . . 7
⊢ (𝜑 → (((𝑥 ∈ (𝐽‘𝑋) ∧ 𝑧 ∈ (𝐽‘𝑌)) ∧ 〈𝐹, 𝑆〉 = (〈𝑥, 𝑂〉(+g‘𝑈)〈𝑧, 𝑂〉)) ↔ ((𝑥 ∈ (𝐽‘𝑋) ∧ 𝑧 ∈ (𝐽‘𝑌)) ∧ (𝐹 = (𝑥(+g‘𝑉)𝑧) ∧ 𝑆 = 𝑂)))) |
90 | 49, 89 | syl5bb 271 |
. . . . . 6
⊢ (𝜑 → (∃𝑦∃𝑤(𝑦 = 𝑂 ∧ 𝑤 = 𝑂 ∧ ((𝑥 ∈ (𝐽‘𝑋) ∧ 𝑧 ∈ (𝐽‘𝑌)) ∧ 〈𝐹, 𝑆〉 = (〈𝑥, 𝑦〉(+g‘𝑈)〈𝑧, 𝑤〉))) ↔ ((𝑥 ∈ (𝐽‘𝑋) ∧ 𝑧 ∈ (𝐽‘𝑌)) ∧ (𝐹 = (𝑥(+g‘𝑉)𝑧) ∧ 𝑆 = 𝑂)))) |
91 | 36, 90 | bitrd 267 |
. . . . 5
⊢ (𝜑 → (∃𝑦∃𝑤((〈𝑥, 𝑦〉 ∈ (𝐼‘𝑋) ∧ 〈𝑧, 𝑤〉 ∈ (𝐼‘𝑌)) ∧ 〈𝐹, 𝑆〉 = (〈𝑥, 𝑦〉(+g‘𝑈)〈𝑧, 𝑤〉)) ↔ ((𝑥 ∈ (𝐽‘𝑋) ∧ 𝑧 ∈ (𝐽‘𝑌)) ∧ (𝐹 = (𝑥(+g‘𝑉)𝑧) ∧ 𝑆 = 𝑂)))) |
92 | 91 | exbidv 1837 |
. . . 4
⊢ (𝜑 → (∃𝑧∃𝑦∃𝑤((〈𝑥, 𝑦〉 ∈ (𝐼‘𝑋) ∧ 〈𝑧, 𝑤〉 ∈ (𝐼‘𝑌)) ∧ 〈𝐹, 𝑆〉 = (〈𝑥, 𝑦〉(+g‘𝑈)〈𝑧, 𝑤〉)) ↔ ∃𝑧((𝑥 ∈ (𝐽‘𝑋) ∧ 𝑧 ∈ (𝐽‘𝑌)) ∧ (𝐹 = (𝑥(+g‘𝑉)𝑧) ∧ 𝑆 = 𝑂)))) |
93 | 18, 92 | syl5bb 271 |
. . 3
⊢ (𝜑 → (∃𝑦∃𝑧∃𝑤((〈𝑥, 𝑦〉 ∈ (𝐼‘𝑋) ∧ 〈𝑧, 𝑤〉 ∈ (𝐼‘𝑌)) ∧ 〈𝐹, 𝑆〉 = (〈𝑥, 𝑦〉(+g‘𝑈)〈𝑧, 𝑤〉)) ↔ ∃𝑧((𝑥 ∈ (𝐽‘𝑋) ∧ 𝑧 ∈ (𝐽‘𝑌)) ∧ (𝐹 = (𝑥(+g‘𝑉)𝑧) ∧ 𝑆 = 𝑂)))) |
94 | 93 | exbidv 1837 |
. 2
⊢ (𝜑 → (∃𝑥∃𝑦∃𝑧∃𝑤((〈𝑥, 𝑦〉 ∈ (𝐼‘𝑋) ∧ 〈𝑧, 𝑤〉 ∈ (𝐼‘𝑌)) ∧ 〈𝐹, 𝑆〉 = (〈𝑥, 𝑦〉(+g‘𝑈)〈𝑧, 𝑤〉)) ↔ ∃𝑥∃𝑧((𝑥 ∈ (𝐽‘𝑋) ∧ 𝑧 ∈ (𝐽‘𝑌)) ∧ (𝐹 = (𝑥(+g‘𝑉)𝑧) ∧ 𝑆 = 𝑂)))) |
95 | | anass 679 |
. . . . . 6
⊢ ((((𝑥 ∈ (𝐽‘𝑋) ∧ 𝑧 ∈ (𝐽‘𝑌)) ∧ 𝐹 = (𝑥(+g‘𝑉)𝑧)) ∧ 𝑆 = 𝑂) ↔ ((𝑥 ∈ (𝐽‘𝑋) ∧ 𝑧 ∈ (𝐽‘𝑌)) ∧ (𝐹 = (𝑥(+g‘𝑉)𝑧) ∧ 𝑆 = 𝑂))) |
96 | 95 | bicomi 213 |
. . . . 5
⊢ (((𝑥 ∈ (𝐽‘𝑋) ∧ 𝑧 ∈ (𝐽‘𝑌)) ∧ (𝐹 = (𝑥(+g‘𝑉)𝑧) ∧ 𝑆 = 𝑂)) ↔ (((𝑥 ∈ (𝐽‘𝑋) ∧ 𝑧 ∈ (𝐽‘𝑌)) ∧ 𝐹 = (𝑥(+g‘𝑉)𝑧)) ∧ 𝑆 = 𝑂)) |
97 | 96 | 2exbii 1765 |
. . . 4
⊢
(∃𝑥∃𝑧((𝑥 ∈ (𝐽‘𝑋) ∧ 𝑧 ∈ (𝐽‘𝑌)) ∧ (𝐹 = (𝑥(+g‘𝑉)𝑧) ∧ 𝑆 = 𝑂)) ↔ ∃𝑥∃𝑧(((𝑥 ∈ (𝐽‘𝑋) ∧ 𝑧 ∈ (𝐽‘𝑌)) ∧ 𝐹 = (𝑥(+g‘𝑉)𝑧)) ∧ 𝑆 = 𝑂)) |
98 | | 19.41vv 1902 |
. . . 4
⊢
(∃𝑥∃𝑧(((𝑥 ∈ (𝐽‘𝑋) ∧ 𝑧 ∈ (𝐽‘𝑌)) ∧ 𝐹 = (𝑥(+g‘𝑉)𝑧)) ∧ 𝑆 = 𝑂) ↔ (∃𝑥∃𝑧((𝑥 ∈ (𝐽‘𝑋) ∧ 𝑧 ∈ (𝐽‘𝑌)) ∧ 𝐹 = (𝑥(+g‘𝑉)𝑧)) ∧ 𝑆 = 𝑂)) |
99 | 97, 98 | bitri 263 |
. . 3
⊢
(∃𝑥∃𝑧((𝑥 ∈ (𝐽‘𝑋) ∧ 𝑧 ∈ (𝐽‘𝑌)) ∧ (𝐹 = (𝑥(+g‘𝑉)𝑧) ∧ 𝑆 = 𝑂)) ↔ (∃𝑥∃𝑧((𝑥 ∈ (𝐽‘𝑋) ∧ 𝑧 ∈ (𝐽‘𝑌)) ∧ 𝐹 = (𝑥(+g‘𝑉)𝑧)) ∧ 𝑆 = 𝑂)) |
100 | 5, 72 | dvalvec 35333 |
. . . . . . . . 9
⊢ ((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) → 𝑉 ∈ LVec) |
101 | | lveclmod 18927 |
. . . . . . . . 9
⊢ (𝑉 ∈ LVec → 𝑉 ∈ LMod) |
102 | | eqid 2610 |
. . . . . . . . . 10
⊢
(LSubSp‘𝑉) =
(LSubSp‘𝑉) |
103 | 102 | lsssssubg 18779 |
. . . . . . . . 9
⊢ (𝑉 ∈ LMod →
(LSubSp‘𝑉) ⊆
(SubGrp‘𝑉)) |
104 | 1, 100, 101, 103 | 4syl 19 |
. . . . . . . 8
⊢ (𝜑 → (LSubSp‘𝑉) ⊆ (SubGrp‘𝑉)) |
105 | 3, 4, 5, 72, 21, 102 | dialss 35353 |
. . . . . . . . 9
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ 𝑋 ≤ 𝑊)) → (𝐽‘𝑋) ∈ (LSubSp‘𝑉)) |
106 | 1, 2, 105 | syl2anc 691 |
. . . . . . . 8
⊢ (𝜑 → (𝐽‘𝑋) ∈ (LSubSp‘𝑉)) |
107 | 104, 106 | sseldd 3569 |
. . . . . . 7
⊢ (𝜑 → (𝐽‘𝑋) ∈ (SubGrp‘𝑉)) |
108 | 3, 4, 5, 72, 21, 102 | dialss 35353 |
. . . . . . . . 9
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑌 ∈ 𝐵 ∧ 𝑌 ≤ 𝑊)) → (𝐽‘𝑌) ∈ (LSubSp‘𝑉)) |
109 | 1, 11, 108 | syl2anc 691 |
. . . . . . . 8
⊢ (𝜑 → (𝐽‘𝑌) ∈ (LSubSp‘𝑉)) |
110 | 104, 109 | sseldd 3569 |
. . . . . . 7
⊢ (𝜑 → (𝐽‘𝑌) ∈ (SubGrp‘𝑉)) |
111 | | diblsmopel.q |
. . . . . . . 8
⊢ ⊕ =
(LSSum‘𝑉) |
112 | 73, 111 | lsmelval 17887 |
. . . . . . 7
⊢ (((𝐽‘𝑋) ∈ (SubGrp‘𝑉) ∧ (𝐽‘𝑌) ∈ (SubGrp‘𝑉)) → (𝐹 ∈ ((𝐽‘𝑋) ⊕ (𝐽‘𝑌)) ↔ ∃𝑥 ∈ (𝐽‘𝑋)∃𝑧 ∈ (𝐽‘𝑌)𝐹 = (𝑥(+g‘𝑉)𝑧))) |
113 | 107, 110,
112 | syl2anc 691 |
. . . . . 6
⊢ (𝜑 → (𝐹 ∈ ((𝐽‘𝑋) ⊕ (𝐽‘𝑌)) ↔ ∃𝑥 ∈ (𝐽‘𝑋)∃𝑧 ∈ (𝐽‘𝑌)𝐹 = (𝑥(+g‘𝑉)𝑧))) |
114 | | r2ex 3043 |
. . . . . 6
⊢
(∃𝑥 ∈
(𝐽‘𝑋)∃𝑧 ∈ (𝐽‘𝑌)𝐹 = (𝑥(+g‘𝑉)𝑧) ↔ ∃𝑥∃𝑧((𝑥 ∈ (𝐽‘𝑋) ∧ 𝑧 ∈ (𝐽‘𝑌)) ∧ 𝐹 = (𝑥(+g‘𝑉)𝑧))) |
115 | 113, 114 | syl6bb 275 |
. . . . 5
⊢ (𝜑 → (𝐹 ∈ ((𝐽‘𝑋) ⊕ (𝐽‘𝑌)) ↔ ∃𝑥∃𝑧((𝑥 ∈ (𝐽‘𝑋) ∧ 𝑧 ∈ (𝐽‘𝑌)) ∧ 𝐹 = (𝑥(+g‘𝑉)𝑧)))) |
116 | 115 | anbi1d 737 |
. . . 4
⊢ (𝜑 → ((𝐹 ∈ ((𝐽‘𝑋) ⊕ (𝐽‘𝑌)) ∧ 𝑆 = 𝑂) ↔ (∃𝑥∃𝑧((𝑥 ∈ (𝐽‘𝑋) ∧ 𝑧 ∈ (𝐽‘𝑌)) ∧ 𝐹 = (𝑥(+g‘𝑉)𝑧)) ∧ 𝑆 = 𝑂))) |
117 | 116 | bicomd 212 |
. . 3
⊢ (𝜑 → ((∃𝑥∃𝑧((𝑥 ∈ (𝐽‘𝑋) ∧ 𝑧 ∈ (𝐽‘𝑌)) ∧ 𝐹 = (𝑥(+g‘𝑉)𝑧)) ∧ 𝑆 = 𝑂) ↔ (𝐹 ∈ ((𝐽‘𝑋) ⊕ (𝐽‘𝑌)) ∧ 𝑆 = 𝑂))) |
118 | 99, 117 | syl5bb 271 |
. 2
⊢ (𝜑 → (∃𝑥∃𝑧((𝑥 ∈ (𝐽‘𝑋) ∧ 𝑧 ∈ (𝐽‘𝑌)) ∧ (𝐹 = (𝑥(+g‘𝑉)𝑧) ∧ 𝑆 = 𝑂)) ↔ (𝐹 ∈ ((𝐽‘𝑋) ⊕ (𝐽‘𝑌)) ∧ 𝑆 = 𝑂))) |
119 | 17, 94, 118 | 3bitrd 293 |
1
⊢ (𝜑 → (〈𝐹, 𝑆〉 ∈ ((𝐼‘𝑋) ✚ (𝐼‘𝑌)) ↔ (𝐹 ∈ ((𝐽‘𝑋) ⊕ (𝐽‘𝑌)) ∧ 𝑆 = 𝑂))) |