Metamath Proof Explorer


Theorem xihopellsmN

Description: Ordered pair membership in a subspace sum of isomorphism H values. (Contributed by NM, 26-Sep-2014) (New usage is discouraged.)

Ref Expression
Hypotheses xihopellsm.b 𝐵 = ( Base ‘ 𝐾 )
xihopellsm.h 𝐻 = ( LHyp ‘ 𝐾 )
xihopellsm.t 𝑇 = ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 )
xihopellsm.e 𝐸 = ( ( TEndo ‘ 𝐾 ) ‘ 𝑊 )
xihopellsm.a 𝐴 = ( 𝑠𝐸 , 𝑡𝐸 ↦ ( 𝑓𝑇 ↦ ( ( 𝑠𝑓 ) ∘ ( 𝑡𝑓 ) ) ) )
xihopellsm.u 𝑈 = ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 )
xihopellsm.l 𝐿 = ( LSubSp ‘ 𝑈 )
xihopellsm.p = ( LSSum ‘ 𝑈 )
xihopellsm.i 𝐼 = ( ( DIsoH ‘ 𝐾 ) ‘ 𝑊 )
xihopellsm.k ( 𝜑 → ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) )
xihopellsm.x ( 𝜑𝑋𝐵 )
xihopellsm.y ( 𝜑𝑌𝐵 )
Assertion xihopellsmN ( 𝜑 → ( ⟨ 𝐹 , 𝑆 ⟩ ∈ ( ( 𝐼𝑋 ) ( 𝐼𝑌 ) ) ↔ ∃ 𝑔𝑡𝑢 ( ( ⟨ 𝑔 , 𝑡 ⟩ ∈ ( 𝐼𝑋 ) ∧ ⟨ , 𝑢 ⟩ ∈ ( 𝐼𝑌 ) ) ∧ ( 𝐹 = ( 𝑔 ) ∧ 𝑆 = ( 𝑡 𝐴 𝑢 ) ) ) ) )

Proof

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 ( 𝜑 → ( ⟨ 𝐹 , 𝑆 ⟩ ∈ ( ( 𝐼𝑋 ) ( 𝐼𝑌 ) ) ↔ ∃ 𝑔𝑡𝑢 ( ( ⟨ 𝑔 , 𝑡 ⟩ ∈ ( 𝐼𝑋 ) ∧ ⟨ , 𝑢 ⟩ ∈ ( 𝐼𝑌 ) ) ∧ ( 𝐹 = ( 𝑔 ) ∧ 𝑆 = ( 𝑡 𝐴 𝑢 ) ) ) ) )