Step |
Hyp |
Ref |
Expression |
1 |
|
xihopellsm.b |
⊢ 𝐵 = ( Base ‘ 𝐾 ) |
2 |
|
xihopellsm.h |
⊢ 𝐻 = ( LHyp ‘ 𝐾 ) |
3 |
|
xihopellsm.t |
⊢ 𝑇 = ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) |
4 |
|
xihopellsm.e |
⊢ 𝐸 = ( ( TEndo ‘ 𝐾 ) ‘ 𝑊 ) |
5 |
|
xihopellsm.a |
⊢ 𝐴 = ( 𝑠 ∈ 𝐸 , 𝑡 ∈ 𝐸 ↦ ( 𝑓 ∈ 𝑇 ↦ ( ( 𝑠 ‘ 𝑓 ) ∘ ( 𝑡 ‘ 𝑓 ) ) ) ) |
6 |
|
xihopellsm.u |
⊢ 𝑈 = ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 ) |
7 |
|
xihopellsm.l |
⊢ 𝐿 = ( LSubSp ‘ 𝑈 ) |
8 |
|
xihopellsm.p |
⊢ ⊕ = ( LSSum ‘ 𝑈 ) |
9 |
|
xihopellsm.i |
⊢ 𝐼 = ( ( DIsoH ‘ 𝐾 ) ‘ 𝑊 ) |
10 |
|
xihopellsm.k |
⊢ ( 𝜑 → ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ) |
11 |
|
xihopellsm.x |
⊢ ( 𝜑 → 𝑋 ∈ 𝐵 ) |
12 |
|
xihopellsm.y |
⊢ ( 𝜑 → 𝑌 ∈ 𝐵 ) |
13 |
|
eqid |
⊢ ( LSubSp ‘ 𝑈 ) = ( LSubSp ‘ 𝑈 ) |
14 |
1 2 9 6 13
|
dihlss |
⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑋 ∈ 𝐵 ) → ( 𝐼 ‘ 𝑋 ) ∈ ( LSubSp ‘ 𝑈 ) ) |
15 |
10 11 14
|
syl2anc |
⊢ ( 𝜑 → ( 𝐼 ‘ 𝑋 ) ∈ ( LSubSp ‘ 𝑈 ) ) |
16 |
1 2 9 6 13
|
dihlss |
⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑌 ∈ 𝐵 ) → ( 𝐼 ‘ 𝑌 ) ∈ ( LSubSp ‘ 𝑈 ) ) |
17 |
10 12 16
|
syl2anc |
⊢ ( 𝜑 → ( 𝐼 ‘ 𝑌 ) ∈ ( LSubSp ‘ 𝑈 ) ) |
18 |
|
eqid |
⊢ ( +g ‘ 𝑈 ) = ( +g ‘ 𝑈 ) |
19 |
2 6 18 13 8
|
dvhopellsm |
⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝐼 ‘ 𝑋 ) ∈ ( LSubSp ‘ 𝑈 ) ∧ ( 𝐼 ‘ 𝑌 ) ∈ ( LSubSp ‘ 𝑈 ) ) → ( 〈 𝐹 , 𝑆 〉 ∈ ( ( 𝐼 ‘ 𝑋 ) ⊕ ( 𝐼 ‘ 𝑌 ) ) ↔ ∃ 𝑔 ∃ 𝑡 ∃ ℎ ∃ 𝑢 ( ( 〈 𝑔 , 𝑡 〉 ∈ ( 𝐼 ‘ 𝑋 ) ∧ 〈 ℎ , 𝑢 〉 ∈ ( 𝐼 ‘ 𝑌 ) ) ∧ 〈 𝐹 , 𝑆 〉 = ( 〈 𝑔 , 𝑡 〉 ( +g ‘ 𝑈 ) 〈 ℎ , 𝑢 〉 ) ) ) ) |
20 |
10 15 17 19
|
syl3anc |
⊢ ( 𝜑 → ( 〈 𝐹 , 𝑆 〉 ∈ ( ( 𝐼 ‘ 𝑋 ) ⊕ ( 𝐼 ‘ 𝑌 ) ) ↔ ∃ 𝑔 ∃ 𝑡 ∃ ℎ ∃ 𝑢 ( ( 〈 𝑔 , 𝑡 〉 ∈ ( 𝐼 ‘ 𝑋 ) ∧ 〈 ℎ , 𝑢 〉 ∈ ( 𝐼 ‘ 𝑌 ) ) ∧ 〈 𝐹 , 𝑆 〉 = ( 〈 𝑔 , 𝑡 〉 ( +g ‘ 𝑈 ) 〈 ℎ , 𝑢 〉 ) ) ) ) |
21 |
10
|
adantr |
⊢ ( ( 𝜑 ∧ 〈 𝑔 , 𝑡 〉 ∈ ( 𝐼 ‘ 𝑋 ) ) → ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ) |
22 |
11
|
adantr |
⊢ ( ( 𝜑 ∧ 〈 𝑔 , 𝑡 〉 ∈ ( 𝐼 ‘ 𝑋 ) ) → 𝑋 ∈ 𝐵 ) |
23 |
|
simpr |
⊢ ( ( 𝜑 ∧ 〈 𝑔 , 𝑡 〉 ∈ ( 𝐼 ‘ 𝑋 ) ) → 〈 𝑔 , 𝑡 〉 ∈ ( 𝐼 ‘ 𝑋 ) ) |
24 |
1 2 3 4 9 21 22 23
|
dihopcl |
⊢ ( ( 𝜑 ∧ 〈 𝑔 , 𝑡 〉 ∈ ( 𝐼 ‘ 𝑋 ) ) → ( 𝑔 ∈ 𝑇 ∧ 𝑡 ∈ 𝐸 ) ) |
25 |
10
|
adantr |
⊢ ( ( 𝜑 ∧ 〈 ℎ , 𝑢 〉 ∈ ( 𝐼 ‘ 𝑌 ) ) → ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ) |
26 |
12
|
adantr |
⊢ ( ( 𝜑 ∧ 〈 ℎ , 𝑢 〉 ∈ ( 𝐼 ‘ 𝑌 ) ) → 𝑌 ∈ 𝐵 ) |
27 |
|
simpr |
⊢ ( ( 𝜑 ∧ 〈 ℎ , 𝑢 〉 ∈ ( 𝐼 ‘ 𝑌 ) ) → 〈 ℎ , 𝑢 〉 ∈ ( 𝐼 ‘ 𝑌 ) ) |
28 |
1 2 3 4 9 25 26 27
|
dihopcl |
⊢ ( ( 𝜑 ∧ 〈 ℎ , 𝑢 〉 ∈ ( 𝐼 ‘ 𝑌 ) ) → ( ℎ ∈ 𝑇 ∧ 𝑢 ∈ 𝐸 ) ) |
29 |
24 28
|
anim12dan |
⊢ ( ( 𝜑 ∧ ( 〈 𝑔 , 𝑡 〉 ∈ ( 𝐼 ‘ 𝑋 ) ∧ 〈 ℎ , 𝑢 〉 ∈ ( 𝐼 ‘ 𝑌 ) ) ) → ( ( 𝑔 ∈ 𝑇 ∧ 𝑡 ∈ 𝐸 ) ∧ ( ℎ ∈ 𝑇 ∧ 𝑢 ∈ 𝐸 ) ) ) |
30 |
10
|
adantr |
⊢ ( ( 𝜑 ∧ ( ( 𝑔 ∈ 𝑇 ∧ 𝑡 ∈ 𝐸 ) ∧ ( ℎ ∈ 𝑇 ∧ 𝑢 ∈ 𝐸 ) ) ) → ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ) |
31 |
|
simprl |
⊢ ( ( 𝜑 ∧ ( ( 𝑔 ∈ 𝑇 ∧ 𝑡 ∈ 𝐸 ) ∧ ( ℎ ∈ 𝑇 ∧ 𝑢 ∈ 𝐸 ) ) ) → ( 𝑔 ∈ 𝑇 ∧ 𝑡 ∈ 𝐸 ) ) |
32 |
|
simprr |
⊢ ( ( 𝜑 ∧ ( ( 𝑔 ∈ 𝑇 ∧ 𝑡 ∈ 𝐸 ) ∧ ( ℎ ∈ 𝑇 ∧ 𝑢 ∈ 𝐸 ) ) ) → ( ℎ ∈ 𝑇 ∧ 𝑢 ∈ 𝐸 ) ) |
33 |
2 3 4 5 6 18
|
dvhopvadd2 |
⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑔 ∈ 𝑇 ∧ 𝑡 ∈ 𝐸 ) ∧ ( ℎ ∈ 𝑇 ∧ 𝑢 ∈ 𝐸 ) ) → ( 〈 𝑔 , 𝑡 〉 ( +g ‘ 𝑈 ) 〈 ℎ , 𝑢 〉 ) = 〈 ( 𝑔 ∘ ℎ ) , ( 𝑡 𝐴 𝑢 ) 〉 ) |
34 |
30 31 32 33
|
syl3anc |
⊢ ( ( 𝜑 ∧ ( ( 𝑔 ∈ 𝑇 ∧ 𝑡 ∈ 𝐸 ) ∧ ( ℎ ∈ 𝑇 ∧ 𝑢 ∈ 𝐸 ) ) ) → ( 〈 𝑔 , 𝑡 〉 ( +g ‘ 𝑈 ) 〈 ℎ , 𝑢 〉 ) = 〈 ( 𝑔 ∘ ℎ ) , ( 𝑡 𝐴 𝑢 ) 〉 ) |
35 |
34
|
eqeq2d |
⊢ ( ( 𝜑 ∧ ( ( 𝑔 ∈ 𝑇 ∧ 𝑡 ∈ 𝐸 ) ∧ ( ℎ ∈ 𝑇 ∧ 𝑢 ∈ 𝐸 ) ) ) → ( 〈 𝐹 , 𝑆 〉 = ( 〈 𝑔 , 𝑡 〉 ( +g ‘ 𝑈 ) 〈 ℎ , 𝑢 〉 ) ↔ 〈 𝐹 , 𝑆 〉 = 〈 ( 𝑔 ∘ ℎ ) , ( 𝑡 𝐴 𝑢 ) 〉 ) ) |
36 |
|
vex |
⊢ 𝑔 ∈ V |
37 |
|
vex |
⊢ ℎ ∈ V |
38 |
36 37
|
coex |
⊢ ( 𝑔 ∘ ℎ ) ∈ V |
39 |
|
ovex |
⊢ ( 𝑡 𝐴 𝑢 ) ∈ V |
40 |
38 39
|
opth2 |
⊢ ( 〈 𝐹 , 𝑆 〉 = 〈 ( 𝑔 ∘ ℎ ) , ( 𝑡 𝐴 𝑢 ) 〉 ↔ ( 𝐹 = ( 𝑔 ∘ ℎ ) ∧ 𝑆 = ( 𝑡 𝐴 𝑢 ) ) ) |
41 |
35 40
|
bitrdi |
⊢ ( ( 𝜑 ∧ ( ( 𝑔 ∈ 𝑇 ∧ 𝑡 ∈ 𝐸 ) ∧ ( ℎ ∈ 𝑇 ∧ 𝑢 ∈ 𝐸 ) ) ) → ( 〈 𝐹 , 𝑆 〉 = ( 〈 𝑔 , 𝑡 〉 ( +g ‘ 𝑈 ) 〈 ℎ , 𝑢 〉 ) ↔ ( 𝐹 = ( 𝑔 ∘ ℎ ) ∧ 𝑆 = ( 𝑡 𝐴 𝑢 ) ) ) ) |
42 |
29 41
|
syldan |
⊢ ( ( 𝜑 ∧ ( 〈 𝑔 , 𝑡 〉 ∈ ( 𝐼 ‘ 𝑋 ) ∧ 〈 ℎ , 𝑢 〉 ∈ ( 𝐼 ‘ 𝑌 ) ) ) → ( 〈 𝐹 , 𝑆 〉 = ( 〈 𝑔 , 𝑡 〉 ( +g ‘ 𝑈 ) 〈 ℎ , 𝑢 〉 ) ↔ ( 𝐹 = ( 𝑔 ∘ ℎ ) ∧ 𝑆 = ( 𝑡 𝐴 𝑢 ) ) ) ) |
43 |
42
|
pm5.32da |
⊢ ( 𝜑 → ( ( ( 〈 𝑔 , 𝑡 〉 ∈ ( 𝐼 ‘ 𝑋 ) ∧ 〈 ℎ , 𝑢 〉 ∈ ( 𝐼 ‘ 𝑌 ) ) ∧ 〈 𝐹 , 𝑆 〉 = ( 〈 𝑔 , 𝑡 〉 ( +g ‘ 𝑈 ) 〈 ℎ , 𝑢 〉 ) ) ↔ ( ( 〈 𝑔 , 𝑡 〉 ∈ ( 𝐼 ‘ 𝑋 ) ∧ 〈 ℎ , 𝑢 〉 ∈ ( 𝐼 ‘ 𝑌 ) ) ∧ ( 𝐹 = ( 𝑔 ∘ ℎ ) ∧ 𝑆 = ( 𝑡 𝐴 𝑢 ) ) ) ) ) |
44 |
43
|
4exbidv |
⊢ ( 𝜑 → ( ∃ 𝑔 ∃ 𝑡 ∃ ℎ ∃ 𝑢 ( ( 〈 𝑔 , 𝑡 〉 ∈ ( 𝐼 ‘ 𝑋 ) ∧ 〈 ℎ , 𝑢 〉 ∈ ( 𝐼 ‘ 𝑌 ) ) ∧ 〈 𝐹 , 𝑆 〉 = ( 〈 𝑔 , 𝑡 〉 ( +g ‘ 𝑈 ) 〈 ℎ , 𝑢 〉 ) ) ↔ ∃ 𝑔 ∃ 𝑡 ∃ ℎ ∃ 𝑢 ( ( 〈 𝑔 , 𝑡 〉 ∈ ( 𝐼 ‘ 𝑋 ) ∧ 〈 ℎ , 𝑢 〉 ∈ ( 𝐼 ‘ 𝑌 ) ) ∧ ( 𝐹 = ( 𝑔 ∘ ℎ ) ∧ 𝑆 = ( 𝑡 𝐴 𝑢 ) ) ) ) ) |
45 |
20 44
|
bitrd |
⊢ ( 𝜑 → ( 〈 𝐹 , 𝑆 〉 ∈ ( ( 𝐼 ‘ 𝑋 ) ⊕ ( 𝐼 ‘ 𝑌 ) ) ↔ ∃ 𝑔 ∃ 𝑡 ∃ ℎ ∃ 𝑢 ( ( 〈 𝑔 , 𝑡 〉 ∈ ( 𝐼 ‘ 𝑋 ) ∧ 〈 ℎ , 𝑢 〉 ∈ ( 𝐼 ‘ 𝑌 ) ) ∧ ( 𝐹 = ( 𝑔 ∘ ℎ ) ∧ 𝑆 = ( 𝑡 𝐴 𝑢 ) ) ) ) ) |