Metamath Proof Explorer

Theorem dihopellsm

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

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

Proof

Step Hyp Ref Expression
1 dihopellsm.b ⊢ 𝐵 = ( Base ‘ 𝐾 )
2 dihopellsm.h ⊢ 𝐻 = ( LHyp ‘ 𝐾 )
3 dihopellsm.t ⊢ 𝑇 = ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 )
4 dihopellsm.e ⊢ 𝐸 = ( ( TEndo ‘ 𝐾 ) ‘ 𝑊 )
5 dihopellsm.a ⊢ 𝐴 = ( 𝑣 ∈ 𝐸 , 𝑤 ∈ 𝐸 ↦ ( 𝑖 ∈ 𝑇 ↦ ( ( 𝑣 ‘ 𝑖 ) ∘ ( 𝑤 ‘ 𝑖 ) ) ) )
6 dihopellsm.u ⊢ 𝑈 = ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 )
7 dihopellsm.l ⊢ 𝐿 = ( LSubSp ‘ 𝑈 )
8 dihopellsm.p ⊢ ⊕ = ( LSSum ‘ 𝑈 )
9 dihopellsm.i ⊢ 𝐼 = ( ( DIsoH ‘ 𝐾 ) ‘ 𝑊 )
10 dihopellsm.k ⊢ ( 𝜑 → ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) )
11 dihopellsm.x ⊢ ( 𝜑 → 𝑋 ∈ 𝐵 )
12 dihopellsm.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 syl6bb ⊢ ( ( 𝜑 ∧ ( ( 𝑔 ∈ 𝑇 ∧ 𝑡 ∈ 𝐸 ) ∧ ( ℎ ∈ 𝑇 ∧ 𝑢 ∈ 𝐸 ) ) ) → ( ⟨ 𝐹 , 𝑆 ⟩ = ( ⟨ 𝑔 , 𝑡 ⟩ ( +g ‘ 𝑈 ) ⟨ ℎ , 𝑢 ⟩ ) ↔ ( 𝐹 = ( 𝑔 ∘ ℎ ) ∧ 𝑆 = ( 𝑡 𝐴 𝑢 ) ) ) )
42 29 41 syldan ⊢ ( ( 𝜑 ∧ ( ⟨ 𝑔 , 𝑡 ⟩ ∈ ( 𝐼 ‘ 𝑋 ) ∧ ⟨ ℎ , 𝑢 ⟩ ∈ ( 𝐼 ‘ 𝑌 ) ) ) → ( ⟨ 𝐹 , 𝑆 ⟩ = ( ⟨ 𝑔 , 𝑡 ⟩ ( +g ‘ 𝑈 ) ⟨ ℎ , 𝑢 ⟩ ) ↔ ( 𝐹 = ( 𝑔 ∘ ℎ ) ∧ 𝑆 = ( 𝑡 𝐴 𝑢 ) ) ) )
43 42 pm5.32da ⊢ ( 𝜑 → ( ( ( ⟨ 𝑔 , 𝑡 ⟩ ∈ ( 𝐼 ‘ 𝑋 ) ∧ ⟨ ℎ , 𝑢 ⟩ ∈ ( 𝐼 ‘ 𝑌 ) ) ∧ ⟨ 𝐹 , 𝑆 ⟩ = ( ⟨ 𝑔 , 𝑡 ⟩ ( +g ‘ 𝑈 ) ⟨ ℎ , 𝑢 ⟩ ) ) ↔ ( ( ⟨ 𝑔 , 𝑡 ⟩ ∈ ( 𝐼 ‘ 𝑋 ) ∧ ⟨ ℎ , 𝑢 ⟩ ∈ ( 𝐼 ‘ 𝑌 ) ) ∧ ( 𝐹 = ( 𝑔 ∘ ℎ ) ∧ 𝑆 = ( 𝑡 𝐴 𝑢 ) ) ) ) )
44 43 4exbidv ⊢ ( 𝜑 → ( ∃ 𝑔 ∃ 𝑡 ∃ ℎ ∃ 𝑢 ( ( ⟨ 𝑔 , 𝑡 ⟩ ∈ ( 𝐼 ‘ 𝑋 ) ∧ ⟨ ℎ , 𝑢 ⟩ ∈ ( 𝐼 ‘ 𝑌 ) ) ∧ ⟨ 𝐹 , 𝑆 ⟩ = ( ⟨ 𝑔 , 𝑡 ⟩ ( +g ‘ 𝑈 ) ⟨ ℎ , 𝑢 ⟩ ) ) ↔ ∃ 𝑔 ∃ 𝑡 ∃ ℎ ∃ 𝑢 ( ( ⟨ 𝑔 , 𝑡 ⟩ ∈ ( 𝐼 ‘ 𝑋 ) ∧ ⟨ ℎ , 𝑢 ⟩ ∈ ( 𝐼 ‘ 𝑌 ) ) ∧ ( 𝐹 = ( 𝑔 ∘ ℎ ) ∧ 𝑆 = ( 𝑡 𝐴 𝑢 ) ) ) ) )
45 20 44 bitrd ⊢ ( 𝜑 → ( ⟨ 𝐹 , 𝑆 ⟩ ∈ ( ( 𝐼 ‘ 𝑋 ) ⊕ ( 𝐼 ‘ 𝑌 ) ) ↔ ∃ 𝑔 ∃ 𝑡 ∃ ℎ ∃ 𝑢 ( ( ⟨ 𝑔 , 𝑡 ⟩ ∈ ( 𝐼 ‘ 𝑋 ) ∧ ⟨ ℎ , 𝑢 ⟩ ∈ ( 𝐼 ‘ 𝑌 ) ) ∧ ( 𝐹 = ( 𝑔 ∘ ℎ ) ∧ 𝑆 = ( 𝑡 𝐴 𝑢 ) ) ) ) )