Metamath Proof Explorer

Theorem diblsmopel

Description: Membership in subspace sum for partial isomorphism B. (Contributed by NM, 21-Sep-2014) (Revised by Mario Carneiro, 6-May-2015)

Ref Expression
Hypotheses diblsmopel.b ⊢ 𝐵 = ( Base ‘ 𝐾 )
diblsmopel.l ⊢ ≤ = ( le ‘ 𝐾 )
diblsmopel.h ⊢ 𝐻 = ( LHyp ‘ 𝐾 )
diblsmopel.t ⊢ 𝑇 = ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 )
diblsmopel.o ⊢ 𝑂 = ( 𝑓 ∈ 𝑇 ↦ ( I ↾ 𝐵 ) )
diblsmopel.v ⊢ 𝑉 = ( ( DVecA ‘ 𝐾 ) ‘ 𝑊 )
diblsmopel.u ⊢ 𝑈 = ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 )
diblsmopel.q ⊢ ⊕ = ( LSSum ‘ 𝑉 )
diblsmopel.p ⊢ ✚ = ( LSSum ‘ 𝑈 )
diblsmopel.j ⊢ 𝐽 = ( ( DIsoA ‘ 𝐾 ) ‘ 𝑊 )
diblsmopel.i ⊢ 𝐼 = ( ( DIsoB ‘ 𝐾 ) ‘ 𝑊 )
diblsmopel.k ⊢ ( 𝜑 → ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) )
diblsmopel.x ⊢ ( 𝜑 → ( 𝑋 ∈ 𝐵 ∧ 𝑋 ≤ 𝑊 ) )
diblsmopel.y ⊢ ( 𝜑 → ( 𝑌 ∈ 𝐵 ∧ 𝑌 ≤ 𝑊 ) )
Assertion diblsmopel ( 𝜑 → ( ⟨ 𝐹 , 𝑆 ⟩ ∈ ( ( 𝐼 ‘ 𝑋 ) ✚ ( 𝐼 ‘ 𝑌 ) ) ↔ ( 𝐹 ∈ ( ( 𝐽 ‘ 𝑋 ) ⊕ ( 𝐽 ‘ 𝑌 ) ) ∧ 𝑆 = 𝑂 ) ) )

Proof

Step Hyp Ref Expression
1 diblsmopel.b ⊢ 𝐵 = ( Base ‘ 𝐾 )
2 diblsmopel.l ⊢ ≤ = ( le ‘ 𝐾 )
3 diblsmopel.h ⊢ 𝐻 = ( LHyp ‘ 𝐾 )
4 diblsmopel.t ⊢ 𝑇 = ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 )
5 diblsmopel.o ⊢ 𝑂 = ( 𝑓 ∈ 𝑇 ↦ ( I ↾ 𝐵 ) )
6 diblsmopel.v ⊢ 𝑉 = ( ( DVecA ‘ 𝐾 ) ‘ 𝑊 )
7 diblsmopel.u ⊢ 𝑈 = ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 )
8 diblsmopel.q ⊢ ⊕ = ( LSSum ‘ 𝑉 )
9 diblsmopel.p ⊢ ✚ = ( LSSum ‘ 𝑈 )
10 diblsmopel.j ⊢ 𝐽 = ( ( DIsoA ‘ 𝐾 ) ‘ 𝑊 )
11 diblsmopel.i ⊢ 𝐼 = ( ( DIsoB ‘ 𝐾 ) ‘ 𝑊 )
12 diblsmopel.k ⊢ ( 𝜑 → ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) )
13 diblsmopel.x ⊢ ( 𝜑 → ( 𝑋 ∈ 𝐵 ∧ 𝑋 ≤ 𝑊 ) )
14 diblsmopel.y ⊢ ( 𝜑 → ( 𝑌 ∈ 𝐵 ∧ 𝑌 ≤ 𝑊 ) )
15 eqid ⊢ ( LSubSp ‘ 𝑈 ) = ( LSubSp ‘ 𝑈 )
16 1 2 3 7 11 15 diblss ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑋 ≤ 𝑊 ) ) → ( 𝐼 ‘ 𝑋 ) ∈ ( LSubSp ‘ 𝑈 ) )
17 12 13 16 syl2anc ⊢ ( 𝜑 → ( 𝐼 ‘ 𝑋 ) ∈ ( LSubSp ‘ 𝑈 ) )
18 1 2 3 7 11 15 diblss ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑌 ∈ 𝐵 ∧ 𝑌 ≤ 𝑊 ) ) → ( 𝐼 ‘ 𝑌 ) ∈ ( LSubSp ‘ 𝑈 ) )
19 12 14 18 syl2anc ⊢ ( 𝜑 → ( 𝐼 ‘ 𝑌 ) ∈ ( LSubSp ‘ 𝑈 ) )
20 eqid ⊢ ( +g ‘ 𝑈 ) = ( +g ‘ 𝑈 )
21 3 7 20 15 9 dvhopellsm ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝐼 ‘ 𝑋 ) ∈ ( LSubSp ‘ 𝑈 ) ∧ ( 𝐼 ‘ 𝑌 ) ∈ ( LSubSp ‘ 𝑈 ) ) → ( ⟨ 𝐹 , 𝑆 ⟩ ∈ ( ( 𝐼 ‘ 𝑋 ) ✚ ( 𝐼 ‘ 𝑌 ) ) ↔ ∃ 𝑥 ∃ 𝑦 ∃ 𝑧 ∃ 𝑤 ( ( ⟨ 𝑥 , 𝑦 ⟩ ∈ ( 𝐼 ‘ 𝑋 ) ∧ ⟨ 𝑧 , 𝑤 ⟩ ∈ ( 𝐼 ‘ 𝑌 ) ) ∧ ⟨ 𝐹 , 𝑆 ⟩ = ( ⟨ 𝑥 , 𝑦 ⟩ ( +g ‘ 𝑈 ) ⟨ 𝑧 , 𝑤 ⟩ ) ) ) )
22 12 17 19 21 syl3anc ⊢ ( 𝜑 → ( ⟨ 𝐹 , 𝑆 ⟩ ∈ ( ( 𝐼 ‘ 𝑋 ) ✚ ( 𝐼 ‘ 𝑌 ) ) ↔ ∃ 𝑥 ∃ 𝑦 ∃ 𝑧 ∃ 𝑤 ( ( ⟨ 𝑥 , 𝑦 ⟩ ∈ ( 𝐼 ‘ 𝑋 ) ∧ ⟨ 𝑧 , 𝑤 ⟩ ∈ ( 𝐼 ‘ 𝑌 ) ) ∧ ⟨ 𝐹 , 𝑆 ⟩ = ( ⟨ 𝑥 , 𝑦 ⟩ ( +g ‘ 𝑈 ) ⟨ 𝑧 , 𝑤 ⟩ ) ) ) )
23 excom ⊢ ( ∃ 𝑦 ∃ 𝑧 ∃ 𝑤 ( ( ⟨ 𝑥 , 𝑦 ⟩ ∈ ( 𝐼 ‘ 𝑋 ) ∧ ⟨ 𝑧 , 𝑤 ⟩ ∈ ( 𝐼 ‘ 𝑌 ) ) ∧ ⟨ 𝐹 , 𝑆 ⟩ = ( ⟨ 𝑥 , 𝑦 ⟩ ( +g ‘ 𝑈 ) ⟨ 𝑧 , 𝑤 ⟩ ) ) ↔ ∃ 𝑧 ∃ 𝑦 ∃ 𝑤 ( ( ⟨ 𝑥 , 𝑦 ⟩ ∈ ( 𝐼 ‘ 𝑋 ) ∧ ⟨ 𝑧 , 𝑤 ⟩ ∈ ( 𝐼 ‘ 𝑌 ) ) ∧ ⟨ 𝐹 , 𝑆 ⟩ = ( ⟨ 𝑥 , 𝑦 ⟩ ( +g ‘ 𝑈 ) ⟨ 𝑧 , 𝑤 ⟩ ) ) )
24 1 2 3 4 5 10 11 dibopelval2 ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑋 ≤ 𝑊 ) ) → ( ⟨ 𝑥 , 𝑦 ⟩ ∈ ( 𝐼 ‘ 𝑋 ) ↔ ( 𝑥 ∈ ( 𝐽 ‘ 𝑋 ) ∧ 𝑦 = 𝑂 ) ) )
25 12 13 24 syl2anc ⊢ ( 𝜑 → ( ⟨ 𝑥 , 𝑦 ⟩ ∈ ( 𝐼 ‘ 𝑋 ) ↔ ( 𝑥 ∈ ( 𝐽 ‘ 𝑋 ) ∧ 𝑦 = 𝑂 ) ) )
26 1 2 3 4 5 10 11 dibopelval2 ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑌 ∈ 𝐵 ∧ 𝑌 ≤ 𝑊 ) ) → ( ⟨ 𝑧 , 𝑤 ⟩ ∈ ( 𝐼 ‘ 𝑌 ) ↔ ( 𝑧 ∈ ( 𝐽 ‘ 𝑌 ) ∧ 𝑤 = 𝑂 ) ) )
27 12 14 26 syl2anc ⊢ ( 𝜑 → ( ⟨ 𝑧 , 𝑤 ⟩ ∈ ( 𝐼 ‘ 𝑌 ) ↔ ( 𝑧 ∈ ( 𝐽 ‘ 𝑌 ) ∧ 𝑤 = 𝑂 ) ) )
28 25 27 anbi12d ⊢ ( 𝜑 → ( ( ⟨ 𝑥 , 𝑦 ⟩ ∈ ( 𝐼 ‘ 𝑋 ) ∧ ⟨ 𝑧 , 𝑤 ⟩ ∈ ( 𝐼 ‘ 𝑌 ) ) ↔ ( ( 𝑥 ∈ ( 𝐽 ‘ 𝑋 ) ∧ 𝑦 = 𝑂 ) ∧ ( 𝑧 ∈ ( 𝐽 ‘ 𝑌 ) ∧ 𝑤 = 𝑂 ) ) ) )
29 an4 ⊢ ( ( ( 𝑥 ∈ ( 𝐽 ‘ 𝑋 ) ∧ 𝑦 = 𝑂 ) ∧ ( 𝑧 ∈ ( 𝐽 ‘ 𝑌 ) ∧ 𝑤 = 𝑂 ) ) ↔ ( ( 𝑥 ∈ ( 𝐽 ‘ 𝑋 ) ∧ 𝑧 ∈ ( 𝐽 ‘ 𝑌 ) ) ∧ ( 𝑦 = 𝑂 ∧ 𝑤 = 𝑂 ) ) )
30 ancom ⊢ ( ( ( 𝑥 ∈ ( 𝐽 ‘ 𝑋 ) ∧ 𝑧 ∈ ( 𝐽 ‘ 𝑌 ) ) ∧ ( 𝑦 = 𝑂 ∧ 𝑤 = 𝑂 ) ) ↔ ( ( 𝑦 = 𝑂 ∧ 𝑤 = 𝑂 ) ∧ ( 𝑥 ∈ ( 𝐽 ‘ 𝑋 ) ∧ 𝑧 ∈ ( 𝐽 ‘ 𝑌 ) ) ) )
31 29 30 bitri ⊢ ( ( ( 𝑥 ∈ ( 𝐽 ‘ 𝑋 ) ∧ 𝑦 = 𝑂 ) ∧ ( 𝑧 ∈ ( 𝐽 ‘ 𝑌 ) ∧ 𝑤 = 𝑂 ) ) ↔ ( ( 𝑦 = 𝑂 ∧ 𝑤 = 𝑂 ) ∧ ( 𝑥 ∈ ( 𝐽 ‘ 𝑋 ) ∧ 𝑧 ∈ ( 𝐽 ‘ 𝑌 ) ) ) )
32 28 31 bitrdi ⊢ ( 𝜑 → ( ( ⟨ 𝑥 , 𝑦 ⟩ ∈ ( 𝐼 ‘ 𝑋 ) ∧ ⟨ 𝑧 , 𝑤 ⟩ ∈ ( 𝐼 ‘ 𝑌 ) ) ↔ ( ( 𝑦 = 𝑂 ∧ 𝑤 = 𝑂 ) ∧ ( 𝑥 ∈ ( 𝐽 ‘ 𝑋 ) ∧ 𝑧 ∈ ( 𝐽 ‘ 𝑌 ) ) ) ) )
33 32 anbi1d ⊢ ( 𝜑 → ( ( ( ⟨ 𝑥 , 𝑦 ⟩ ∈ ( 𝐼 ‘ 𝑋 ) ∧ ⟨ 𝑧 , 𝑤 ⟩ ∈ ( 𝐼 ‘ 𝑌 ) ) ∧ ⟨ 𝐹 , 𝑆 ⟩ = ( ⟨ 𝑥 , 𝑦 ⟩ ( +g ‘ 𝑈 ) ⟨ 𝑧 , 𝑤 ⟩ ) ) ↔ ( ( ( 𝑦 = 𝑂 ∧ 𝑤 = 𝑂 ) ∧ ( 𝑥 ∈ ( 𝐽 ‘ 𝑋 ) ∧ 𝑧 ∈ ( 𝐽 ‘ 𝑌 ) ) ) ∧ ⟨ 𝐹 , 𝑆 ⟩ = ( ⟨ 𝑥 , 𝑦 ⟩ ( +g ‘ 𝑈 ) ⟨ 𝑧 , 𝑤 ⟩ ) ) ) )
34 anass ⊢ ( ( ( ( 𝑦 = 𝑂 ∧ 𝑤 = 𝑂 ) ∧ ( 𝑥 ∈ ( 𝐽 ‘ 𝑋 ) ∧ 𝑧 ∈ ( 𝐽 ‘ 𝑌 ) ) ) ∧ ⟨ 𝐹 , 𝑆 ⟩ = ( ⟨ 𝑥 , 𝑦 ⟩ ( +g ‘ 𝑈 ) ⟨ 𝑧 , 𝑤 ⟩ ) ) ↔ ( ( 𝑦 = 𝑂 ∧ 𝑤 = 𝑂 ) ∧ ( ( 𝑥 ∈ ( 𝐽 ‘ 𝑋 ) ∧ 𝑧 ∈ ( 𝐽 ‘ 𝑌 ) ) ∧ ⟨ 𝐹 , 𝑆 ⟩ = ( ⟨ 𝑥 , 𝑦 ⟩ ( +g ‘ 𝑈 ) ⟨ 𝑧 , 𝑤 ⟩ ) ) ) )
35 df-3an ⊢ ( ( 𝑦 = 𝑂 ∧ 𝑤 = 𝑂 ∧ ( ( 𝑥 ∈ ( 𝐽 ‘ 𝑋 ) ∧ 𝑧 ∈ ( 𝐽 ‘ 𝑌 ) ) ∧ ⟨ 𝐹 , 𝑆 ⟩ = ( ⟨ 𝑥 , 𝑦 ⟩ ( +g ‘ 𝑈 ) ⟨ 𝑧 , 𝑤 ⟩ ) ) ) ↔ ( ( 𝑦 = 𝑂 ∧ 𝑤 = 𝑂 ) ∧ ( ( 𝑥 ∈ ( 𝐽 ‘ 𝑋 ) ∧ 𝑧 ∈ ( 𝐽 ‘ 𝑌 ) ) ∧ ⟨ 𝐹 , 𝑆 ⟩ = ( ⟨ 𝑥 , 𝑦 ⟩ ( +g ‘ 𝑈 ) ⟨ 𝑧 , 𝑤 ⟩ ) ) ) )
36 34 35 bitr4i ⊢ ( ( ( ( 𝑦 = 𝑂 ∧ 𝑤 = 𝑂 ) ∧ ( 𝑥 ∈ ( 𝐽 ‘ 𝑋 ) ∧ 𝑧 ∈ ( 𝐽 ‘ 𝑌 ) ) ) ∧ ⟨ 𝐹 , 𝑆 ⟩ = ( ⟨ 𝑥 , 𝑦 ⟩ ( +g ‘ 𝑈 ) ⟨ 𝑧 , 𝑤 ⟩ ) ) ↔ ( 𝑦 = 𝑂 ∧ 𝑤 = 𝑂 ∧ ( ( 𝑥 ∈ ( 𝐽 ‘ 𝑋 ) ∧ 𝑧 ∈ ( 𝐽 ‘ 𝑌 ) ) ∧ ⟨ 𝐹 , 𝑆 ⟩ = ( ⟨ 𝑥 , 𝑦 ⟩ ( +g ‘ 𝑈 ) ⟨ 𝑧 , 𝑤 ⟩ ) ) ) )
37 33 36 bitrdi ⊢ ( 𝜑 → ( ( ( ⟨ 𝑥 , 𝑦 ⟩ ∈ ( 𝐼 ‘ 𝑋 ) ∧ ⟨ 𝑧 , 𝑤 ⟩ ∈ ( 𝐼 ‘ 𝑌 ) ) ∧ ⟨ 𝐹 , 𝑆 ⟩ = ( ⟨ 𝑥 , 𝑦 ⟩ ( +g ‘ 𝑈 ) ⟨ 𝑧 , 𝑤 ⟩ ) ) ↔ ( 𝑦 = 𝑂 ∧ 𝑤 = 𝑂 ∧ ( ( 𝑥 ∈ ( 𝐽 ‘ 𝑋 ) ∧ 𝑧 ∈ ( 𝐽 ‘ 𝑌 ) ) ∧ ⟨ 𝐹 , 𝑆 ⟩ = ( ⟨ 𝑥 , 𝑦 ⟩ ( +g ‘ 𝑈 ) ⟨ 𝑧 , 𝑤 ⟩ ) ) ) ) )
38 37 2exbidv ⊢ ( 𝜑 → ( ∃ 𝑦 ∃ 𝑤 ( ( ⟨ 𝑥 , 𝑦 ⟩ ∈ ( 𝐼 ‘ 𝑋 ) ∧ ⟨ 𝑧 , 𝑤 ⟩ ∈ ( 𝐼 ‘ 𝑌 ) ) ∧ ⟨ 𝐹 , 𝑆 ⟩ = ( ⟨ 𝑥 , 𝑦 ⟩ ( +g ‘ 𝑈 ) ⟨ 𝑧 , 𝑤 ⟩ ) ) ↔ ∃ 𝑦 ∃ 𝑤 ( 𝑦 = 𝑂 ∧ 𝑤 = 𝑂 ∧ ( ( 𝑥 ∈ ( 𝐽 ‘ 𝑋 ) ∧ 𝑧 ∈ ( 𝐽 ‘ 𝑌 ) ) ∧ ⟨ 𝐹 , 𝑆 ⟩ = ( ⟨ 𝑥 , 𝑦 ⟩ ( +g ‘ 𝑈 ) ⟨ 𝑧 , 𝑤 ⟩ ) ) ) ) )
39 4 fvexi ⊢ 𝑇 ∈ V
40 39 mptex ⊢ ( 𝑓 ∈ 𝑇 ↦ ( I ↾ 𝐵 ) ) ∈ V
41 5 40 eqeltri ⊢ 𝑂 ∈ V
42 opeq2 ⊢ ( 𝑦 = 𝑂 → ⟨ 𝑥 , 𝑦 ⟩ = ⟨ 𝑥 , 𝑂 ⟩ )
43 42 oveq1d ⊢ ( 𝑦 = 𝑂 → ( ⟨ 𝑥 , 𝑦 ⟩ ( +g ‘ 𝑈 ) ⟨ 𝑧 , 𝑤 ⟩ ) = ( ⟨ 𝑥 , 𝑂 ⟩ ( +g ‘ 𝑈 ) ⟨ 𝑧 , 𝑤 ⟩ ) )
44 43 eqeq2d ⊢ ( 𝑦 = 𝑂 → ( ⟨ 𝐹 , 𝑆 ⟩ = ( ⟨ 𝑥 , 𝑦 ⟩ ( +g ‘ 𝑈 ) ⟨ 𝑧 , 𝑤 ⟩ ) ↔ ⟨ 𝐹 , 𝑆 ⟩ = ( ⟨ 𝑥 , 𝑂 ⟩ ( +g ‘ 𝑈 ) ⟨ 𝑧 , 𝑤 ⟩ ) ) )
45 44 anbi2d ⊢ ( 𝑦 = 𝑂 → ( ( ( 𝑥 ∈ ( 𝐽 ‘ 𝑋 ) ∧ 𝑧 ∈ ( 𝐽 ‘ 𝑌 ) ) ∧ ⟨ 𝐹 , 𝑆 ⟩ = ( ⟨ 𝑥 , 𝑦 ⟩ ( +g ‘ 𝑈 ) ⟨ 𝑧 , 𝑤 ⟩ ) ) ↔ ( ( 𝑥 ∈ ( 𝐽 ‘ 𝑋 ) ∧ 𝑧 ∈ ( 𝐽 ‘ 𝑌 ) ) ∧ ⟨ 𝐹 , 𝑆 ⟩ = ( ⟨ 𝑥 , 𝑂 ⟩ ( +g ‘ 𝑈 ) ⟨ 𝑧 , 𝑤 ⟩ ) ) ) )
46 opeq2 ⊢ ( 𝑤 = 𝑂 → ⟨ 𝑧 , 𝑤 ⟩ = ⟨ 𝑧 , 𝑂 ⟩ )
47 46 oveq2d ⊢ ( 𝑤 = 𝑂 → ( ⟨ 𝑥 , 𝑂 ⟩ ( +g ‘ 𝑈 ) ⟨ 𝑧 , 𝑤 ⟩ ) = ( ⟨ 𝑥 , 𝑂 ⟩ ( +g ‘ 𝑈 ) ⟨ 𝑧 , 𝑂 ⟩ ) )
48 47 eqeq2d ⊢ ( 𝑤 = 𝑂 → ( ⟨ 𝐹 , 𝑆 ⟩ = ( ⟨ 𝑥 , 𝑂 ⟩ ( +g ‘ 𝑈 ) ⟨ 𝑧 , 𝑤 ⟩ ) ↔ ⟨ 𝐹 , 𝑆 ⟩ = ( ⟨ 𝑥 , 𝑂 ⟩ ( +g ‘ 𝑈 ) ⟨ 𝑧 , 𝑂 ⟩ ) ) )
49 48 anbi2d ⊢ ( 𝑤 = 𝑂 → ( ( ( 𝑥 ∈ ( 𝐽 ‘ 𝑋 ) ∧ 𝑧 ∈ ( 𝐽 ‘ 𝑌 ) ) ∧ ⟨ 𝐹 , 𝑆 ⟩ = ( ⟨ 𝑥 , 𝑂 ⟩ ( +g ‘ 𝑈 ) ⟨ 𝑧 , 𝑤 ⟩ ) ) ↔ ( ( 𝑥 ∈ ( 𝐽 ‘ 𝑋 ) ∧ 𝑧 ∈ ( 𝐽 ‘ 𝑌 ) ) ∧ ⟨ 𝐹 , 𝑆 ⟩ = ( ⟨ 𝑥 , 𝑂 ⟩ ( +g ‘ 𝑈 ) ⟨ 𝑧 , 𝑂 ⟩ ) ) ) )
50 41 41 45 49 ceqsex2v ⊢ ( ∃ 𝑦 ∃ 𝑤 ( 𝑦 = 𝑂 ∧ 𝑤 = 𝑂 ∧ ( ( 𝑥 ∈ ( 𝐽 ‘ 𝑋 ) ∧ 𝑧 ∈ ( 𝐽 ‘ 𝑌 ) ) ∧ ⟨ 𝐹 , 𝑆 ⟩ = ( ⟨ 𝑥 , 𝑦 ⟩ ( +g ‘ 𝑈 ) ⟨ 𝑧 , 𝑤 ⟩ ) ) ) ↔ ( ( 𝑥 ∈ ( 𝐽 ‘ 𝑋 ) ∧ 𝑧 ∈ ( 𝐽 ‘ 𝑌 ) ) ∧ ⟨ 𝐹 , 𝑆 ⟩ = ( ⟨ 𝑥 , 𝑂 ⟩ ( +g ‘ 𝑈 ) ⟨ 𝑧 , 𝑂 ⟩ ) ) )
51 12 adantr ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( 𝐽 ‘ 𝑋 ) ∧ 𝑧 ∈ ( 𝐽 ‘ 𝑌 ) ) ) → ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) )
52 13 adantr ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( 𝐽 ‘ 𝑋 ) ∧ 𝑧 ∈ ( 𝐽 ‘ 𝑌 ) ) ) → ( 𝑋 ∈ 𝐵 ∧ 𝑋 ≤ 𝑊 ) )
53 simprl ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( 𝐽 ‘ 𝑋 ) ∧ 𝑧 ∈ ( 𝐽 ‘ 𝑌 ) ) ) → 𝑥 ∈ ( 𝐽 ‘ 𝑋 ) )
54 1 2 3 4 10 diael ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑋 ≤ 𝑊 ) ∧ 𝑥 ∈ ( 𝐽 ‘ 𝑋 ) ) → 𝑥 ∈ 𝑇 )
55 51 52 53 54 syl3anc ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( 𝐽 ‘ 𝑋 ) ∧ 𝑧 ∈ ( 𝐽 ‘ 𝑌 ) ) ) → 𝑥 ∈ 𝑇 )
56 eqid ⊢ ( ( TEndo ‘ 𝐾 ) ‘ 𝑊 ) = ( ( TEndo ‘ 𝐾 ) ‘ 𝑊 )
57 1 3 4 56 5 tendo0cl ⊢ ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) → 𝑂 ∈ ( ( TEndo ‘ 𝐾 ) ‘ 𝑊 ) )
58 51 57 syl ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( 𝐽 ‘ 𝑋 ) ∧ 𝑧 ∈ ( 𝐽 ‘ 𝑌 ) ) ) → 𝑂 ∈ ( ( TEndo ‘ 𝐾 ) ‘ 𝑊 ) )
59 14 adantr ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( 𝐽 ‘ 𝑋 ) ∧ 𝑧 ∈ ( 𝐽 ‘ 𝑌 ) ) ) → ( 𝑌 ∈ 𝐵 ∧ 𝑌 ≤ 𝑊 ) )
60 simprr ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( 𝐽 ‘ 𝑋 ) ∧ 𝑧 ∈ ( 𝐽 ‘ 𝑌 ) ) ) → 𝑧 ∈ ( 𝐽 ‘ 𝑌 ) )
61 1 2 3 4 10 diael ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑌 ∈ 𝐵 ∧ 𝑌 ≤ 𝑊 ) ∧ 𝑧 ∈ ( 𝐽 ‘ 𝑌 ) ) → 𝑧 ∈ 𝑇 )
62 51 59 60 61 syl3anc ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( 𝐽 ‘ 𝑋 ) ∧ 𝑧 ∈ ( 𝐽 ‘ 𝑌 ) ) ) → 𝑧 ∈ 𝑇 )
63 eqid ⊢ ( Scalar ‘ 𝑈 ) = ( Scalar ‘ 𝑈 )
64 eqid ⊢ ( +g ‘ ( Scalar ‘ 𝑈 ) ) = ( +g ‘ ( Scalar ‘ 𝑈 ) )
65 3 4 56 7 63 20 64 dvhopvadd ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑥 ∈ 𝑇 ∧ 𝑂 ∈ ( ( TEndo ‘ 𝐾 ) ‘ 𝑊 ) ) ∧ ( 𝑧 ∈ 𝑇 ∧ 𝑂 ∈ ( ( TEndo ‘ 𝐾 ) ‘ 𝑊 ) ) ) → ( ⟨ 𝑥 , 𝑂 ⟩ ( +g ‘ 𝑈 ) ⟨ 𝑧 , 𝑂 ⟩ ) = ⟨ ( 𝑥 ∘ 𝑧 ) , ( 𝑂 ( +g ‘ ( Scalar ‘ 𝑈 ) ) 𝑂 ) ⟩ )
66 51 55 58 62 58 65 syl122anc ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( 𝐽 ‘ 𝑋 ) ∧ 𝑧 ∈ ( 𝐽 ‘ 𝑌 ) ) ) → ( ⟨ 𝑥 , 𝑂 ⟩ ( +g ‘ 𝑈 ) ⟨ 𝑧 , 𝑂 ⟩ ) = ⟨ ( 𝑥 ∘ 𝑧 ) , ( 𝑂 ( +g ‘ ( Scalar ‘ 𝑈 ) ) 𝑂 ) ⟩ )
67 66 eqeq2d ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( 𝐽 ‘ 𝑋 ) ∧ 𝑧 ∈ ( 𝐽 ‘ 𝑌 ) ) ) → ( ⟨ 𝐹 , 𝑆 ⟩ = ( ⟨ 𝑥 , 𝑂 ⟩ ( +g ‘ 𝑈 ) ⟨ 𝑧 , 𝑂 ⟩ ) ↔ ⟨ 𝐹 , 𝑆 ⟩ = ⟨ ( 𝑥 ∘ 𝑧 ) , ( 𝑂 ( +g ‘ ( Scalar ‘ 𝑈 ) ) 𝑂 ) ⟩ ) )
68 vex ⊢ 𝑥 ∈ V
69 vex ⊢ 𝑧 ∈ V
70 68 69 coex ⊢ ( 𝑥 ∘ 𝑧 ) ∈ V
71 ovex ⊢ ( 𝑂 ( +g ‘ ( Scalar ‘ 𝑈 ) ) 𝑂 ) ∈ V
72 70 71 opth2 ⊢ ( ⟨ 𝐹 , 𝑆 ⟩ = ⟨ ( 𝑥 ∘ 𝑧 ) , ( 𝑂 ( +g ‘ ( Scalar ‘ 𝑈 ) ) 𝑂 ) ⟩ ↔ ( 𝐹 = ( 𝑥 ∘ 𝑧 ) ∧ 𝑆 = ( 𝑂 ( +g ‘ ( Scalar ‘ 𝑈 ) ) 𝑂 ) ) )
73 eqid ⊢ ( +g ‘ 𝑉 ) = ( +g ‘ 𝑉 )
74 3 4 6 73 dvavadd ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑥 ∈ 𝑇 ∧ 𝑧 ∈ 𝑇 ) ) → ( 𝑥 ( +g ‘ 𝑉 ) 𝑧 ) = ( 𝑥 ∘ 𝑧 ) )
75 51 55 62 74 syl12anc ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( 𝐽 ‘ 𝑋 ) ∧ 𝑧 ∈ ( 𝐽 ‘ 𝑌 ) ) ) → ( 𝑥 ( +g ‘ 𝑉 ) 𝑧 ) = ( 𝑥 ∘ 𝑧 ) )
76 75 eqeq2d ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( 𝐽 ‘ 𝑋 ) ∧ 𝑧 ∈ ( 𝐽 ‘ 𝑌 ) ) ) → ( 𝐹 = ( 𝑥 ( +g ‘ 𝑉 ) 𝑧 ) ↔ 𝐹 = ( 𝑥 ∘ 𝑧 ) ) )
77 76 bicomd ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( 𝐽 ‘ 𝑋 ) ∧ 𝑧 ∈ ( 𝐽 ‘ 𝑌 ) ) ) → ( 𝐹 = ( 𝑥 ∘ 𝑧 ) ↔ 𝐹 = ( 𝑥 ( +g ‘ 𝑉 ) 𝑧 ) ) )
78 eqid ⊢ ( 𝑠 ∈ ( ( TEndo ‘ 𝐾 ) ‘ 𝑊 ) , 𝑡 ∈ ( ( TEndo ‘ 𝐾 ) ‘ 𝑊 ) ↦ ( 𝑓 ∈ 𝑇 ↦ ( ( 𝑠 ‘ 𝑓 ) ∘ ( 𝑡 ‘ 𝑓 ) ) ) ) = ( 𝑠 ∈ ( ( TEndo ‘ 𝐾 ) ‘ 𝑊 ) , 𝑡 ∈ ( ( TEndo ‘ 𝐾 ) ‘ 𝑊 ) ↦ ( 𝑓 ∈ 𝑇 ↦ ( ( 𝑠 ‘ 𝑓 ) ∘ ( 𝑡 ‘ 𝑓 ) ) ) )
79 3 4 56 7 63 78 64 dvhfplusr ⊢ ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) → ( +g ‘ ( Scalar ‘ 𝑈 ) ) = ( 𝑠 ∈ ( ( TEndo ‘ 𝐾 ) ‘ 𝑊 ) , 𝑡 ∈ ( ( TEndo ‘ 𝐾 ) ‘ 𝑊 ) ↦ ( 𝑓 ∈ 𝑇 ↦ ( ( 𝑠 ‘ 𝑓 ) ∘ ( 𝑡 ‘ 𝑓 ) ) ) ) )
80 51 79 syl ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( 𝐽 ‘ 𝑋 ) ∧ 𝑧 ∈ ( 𝐽 ‘ 𝑌 ) ) ) → ( +g ‘ ( Scalar ‘ 𝑈 ) ) = ( 𝑠 ∈ ( ( TEndo ‘ 𝐾 ) ‘ 𝑊 ) , 𝑡 ∈ ( ( TEndo ‘ 𝐾 ) ‘ 𝑊 ) ↦ ( 𝑓 ∈ 𝑇 ↦ ( ( 𝑠 ‘ 𝑓 ) ∘ ( 𝑡 ‘ 𝑓 ) ) ) ) )
81 80 oveqd ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( 𝐽 ‘ 𝑋 ) ∧ 𝑧 ∈ ( 𝐽 ‘ 𝑌 ) ) ) → ( 𝑂 ( +g ‘ ( Scalar ‘ 𝑈 ) ) 𝑂 ) = ( 𝑂 ( 𝑠 ∈ ( ( TEndo ‘ 𝐾 ) ‘ 𝑊 ) , 𝑡 ∈ ( ( TEndo ‘ 𝐾 ) ‘ 𝑊 ) ↦ ( 𝑓 ∈ 𝑇 ↦ ( ( 𝑠 ‘ 𝑓 ) ∘ ( 𝑡 ‘ 𝑓 ) ) ) ) 𝑂 ) )
82 1 3 4 56 5 78 tendo0pl ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑂 ∈ ( ( TEndo ‘ 𝐾 ) ‘ 𝑊 ) ) → ( 𝑂 ( 𝑠 ∈ ( ( TEndo ‘ 𝐾 ) ‘ 𝑊 ) , 𝑡 ∈ ( ( TEndo ‘ 𝐾 ) ‘ 𝑊 ) ↦ ( 𝑓 ∈ 𝑇 ↦ ( ( 𝑠 ‘ 𝑓 ) ∘ ( 𝑡 ‘ 𝑓 ) ) ) ) 𝑂 ) = 𝑂 )
83 51 58 82 syl2anc ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( 𝐽 ‘ 𝑋 ) ∧ 𝑧 ∈ ( 𝐽 ‘ 𝑌 ) ) ) → ( 𝑂 ( 𝑠 ∈ ( ( TEndo ‘ 𝐾 ) ‘ 𝑊 ) , 𝑡 ∈ ( ( TEndo ‘ 𝐾 ) ‘ 𝑊 ) ↦ ( 𝑓 ∈ 𝑇 ↦ ( ( 𝑠 ‘ 𝑓 ) ∘ ( 𝑡 ‘ 𝑓 ) ) ) ) 𝑂 ) = 𝑂 )
84 81 83 eqtrd ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( 𝐽 ‘ 𝑋 ) ∧ 𝑧 ∈ ( 𝐽 ‘ 𝑌 ) ) ) → ( 𝑂 ( +g ‘ ( Scalar ‘ 𝑈 ) ) 𝑂 ) = 𝑂 )
85 84 eqeq2d ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( 𝐽 ‘ 𝑋 ) ∧ 𝑧 ∈ ( 𝐽 ‘ 𝑌 ) ) ) → ( 𝑆 = ( 𝑂 ( +g ‘ ( Scalar ‘ 𝑈 ) ) 𝑂 ) ↔ 𝑆 = 𝑂 ) )
86 77 85 anbi12d ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( 𝐽 ‘ 𝑋 ) ∧ 𝑧 ∈ ( 𝐽 ‘ 𝑌 ) ) ) → ( ( 𝐹 = ( 𝑥 ∘ 𝑧 ) ∧ 𝑆 = ( 𝑂 ( +g ‘ ( Scalar ‘ 𝑈 ) ) 𝑂 ) ) ↔ ( 𝐹 = ( 𝑥 ( +g ‘ 𝑉 ) 𝑧 ) ∧ 𝑆 = 𝑂 ) ) )
87 72 86 syl5bb ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( 𝐽 ‘ 𝑋 ) ∧ 𝑧 ∈ ( 𝐽 ‘ 𝑌 ) ) ) → ( ⟨ 𝐹 , 𝑆 ⟩ = ⟨ ( 𝑥 ∘ 𝑧 ) , ( 𝑂 ( +g ‘ ( Scalar ‘ 𝑈 ) ) 𝑂 ) ⟩ ↔ ( 𝐹 = ( 𝑥 ( +g ‘ 𝑉 ) 𝑧 ) ∧ 𝑆 = 𝑂 ) ) )
88 67 87 bitrd ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( 𝐽 ‘ 𝑋 ) ∧ 𝑧 ∈ ( 𝐽 ‘ 𝑌 ) ) ) → ( ⟨ 𝐹 , 𝑆 ⟩ = ( ⟨ 𝑥 , 𝑂 ⟩ ( +g ‘ 𝑈 ) ⟨ 𝑧 , 𝑂 ⟩ ) ↔ ( 𝐹 = ( 𝑥 ( +g ‘ 𝑉 ) 𝑧 ) ∧ 𝑆 = 𝑂 ) ) )
89 88 pm5.32da ⊢ ( 𝜑 → ( ( ( 𝑥 ∈ ( 𝐽 ‘ 𝑋 ) ∧ 𝑧 ∈ ( 𝐽 ‘ 𝑌 ) ) ∧ ⟨ 𝐹 , 𝑆 ⟩ = ( ⟨ 𝑥 , 𝑂 ⟩ ( +g ‘ 𝑈 ) ⟨ 𝑧 , 𝑂 ⟩ ) ) ↔ ( ( 𝑥 ∈ ( 𝐽 ‘ 𝑋 ) ∧ 𝑧 ∈ ( 𝐽 ‘ 𝑌 ) ) ∧ ( 𝐹 = ( 𝑥 ( +g ‘ 𝑉 ) 𝑧 ) ∧ 𝑆 = 𝑂 ) ) ) )
90 50 89 syl5bb ⊢ ( 𝜑 → ( ∃ 𝑦 ∃ 𝑤 ( 𝑦 = 𝑂 ∧ 𝑤 = 𝑂 ∧ ( ( 𝑥 ∈ ( 𝐽 ‘ 𝑋 ) ∧ 𝑧 ∈ ( 𝐽 ‘ 𝑌 ) ) ∧ ⟨ 𝐹 , 𝑆 ⟩ = ( ⟨ 𝑥 , 𝑦 ⟩ ( +g ‘ 𝑈 ) ⟨ 𝑧 , 𝑤 ⟩ ) ) ) ↔ ( ( 𝑥 ∈ ( 𝐽 ‘ 𝑋 ) ∧ 𝑧 ∈ ( 𝐽 ‘ 𝑌 ) ) ∧ ( 𝐹 = ( 𝑥 ( +g ‘ 𝑉 ) 𝑧 ) ∧ 𝑆 = 𝑂 ) ) ) )
91 38 90 bitrd ⊢ ( 𝜑 → ( ∃ 𝑦 ∃ 𝑤 ( ( ⟨ 𝑥 , 𝑦 ⟩ ∈ ( 𝐼 ‘ 𝑋 ) ∧ ⟨ 𝑧 , 𝑤 ⟩ ∈ ( 𝐼 ‘ 𝑌 ) ) ∧ ⟨ 𝐹 , 𝑆 ⟩ = ( ⟨ 𝑥 , 𝑦 ⟩ ( +g ‘ 𝑈 ) ⟨ 𝑧 , 𝑤 ⟩ ) ) ↔ ( ( 𝑥 ∈ ( 𝐽 ‘ 𝑋 ) ∧ 𝑧 ∈ ( 𝐽 ‘ 𝑌 ) ) ∧ ( 𝐹 = ( 𝑥 ( +g ‘ 𝑉 ) 𝑧 ) ∧ 𝑆 = 𝑂 ) ) ) )
92 91 exbidv ⊢ ( 𝜑 → ( ∃ 𝑧 ∃ 𝑦 ∃ 𝑤 ( ( ⟨ 𝑥 , 𝑦 ⟩ ∈ ( 𝐼 ‘ 𝑋 ) ∧ ⟨ 𝑧 , 𝑤 ⟩ ∈ ( 𝐼 ‘ 𝑌 ) ) ∧ ⟨ 𝐹 , 𝑆 ⟩ = ( ⟨ 𝑥 , 𝑦 ⟩ ( +g ‘ 𝑈 ) ⟨ 𝑧 , 𝑤 ⟩ ) ) ↔ ∃ 𝑧 ( ( 𝑥 ∈ ( 𝐽 ‘ 𝑋 ) ∧ 𝑧 ∈ ( 𝐽 ‘ 𝑌 ) ) ∧ ( 𝐹 = ( 𝑥 ( +g ‘ 𝑉 ) 𝑧 ) ∧ 𝑆 = 𝑂 ) ) ) )
93 23 92 syl5bb ⊢ ( 𝜑 → ( ∃ 𝑦 ∃ 𝑧 ∃ 𝑤 ( ( ⟨ 𝑥 , 𝑦 ⟩ ∈ ( 𝐼 ‘ 𝑋 ) ∧ ⟨ 𝑧 , 𝑤 ⟩ ∈ ( 𝐼 ‘ 𝑌 ) ) ∧ ⟨ 𝐹 , 𝑆 ⟩ = ( ⟨ 𝑥 , 𝑦 ⟩ ( +g ‘ 𝑈 ) ⟨ 𝑧 , 𝑤 ⟩ ) ) ↔ ∃ 𝑧 ( ( 𝑥 ∈ ( 𝐽 ‘ 𝑋 ) ∧ 𝑧 ∈ ( 𝐽 ‘ 𝑌 ) ) ∧ ( 𝐹 = ( 𝑥 ( +g ‘ 𝑉 ) 𝑧 ) ∧ 𝑆 = 𝑂 ) ) ) )
94 93 exbidv ⊢ ( 𝜑 → ( ∃ 𝑥 ∃ 𝑦 ∃ 𝑧 ∃ 𝑤 ( ( ⟨ 𝑥 , 𝑦 ⟩ ∈ ( 𝐼 ‘ 𝑋 ) ∧ ⟨ 𝑧 , 𝑤 ⟩ ∈ ( 𝐼 ‘ 𝑌 ) ) ∧ ⟨ 𝐹 , 𝑆 ⟩ = ( ⟨ 𝑥 , 𝑦 ⟩ ( +g ‘ 𝑈 ) ⟨ 𝑧 , 𝑤 ⟩ ) ) ↔ ∃ 𝑥 ∃ 𝑧 ( ( 𝑥 ∈ ( 𝐽 ‘ 𝑋 ) ∧ 𝑧 ∈ ( 𝐽 ‘ 𝑌 ) ) ∧ ( 𝐹 = ( 𝑥 ( +g ‘ 𝑉 ) 𝑧 ) ∧ 𝑆 = 𝑂 ) ) ) )
95 anass ⊢ ( ( ( ( 𝑥 ∈ ( 𝐽 ‘ 𝑋 ) ∧ 𝑧 ∈ ( 𝐽 ‘ 𝑌 ) ) ∧ 𝐹 = ( 𝑥 ( +g ‘ 𝑉 ) 𝑧 ) ) ∧ 𝑆 = 𝑂 ) ↔ ( ( 𝑥 ∈ ( 𝐽 ‘ 𝑋 ) ∧ 𝑧 ∈ ( 𝐽 ‘ 𝑌 ) ) ∧ ( 𝐹 = ( 𝑥 ( +g ‘ 𝑉 ) 𝑧 ) ∧ 𝑆 = 𝑂 ) ) )
96 95 bicomi ⊢ ( ( ( 𝑥 ∈ ( 𝐽 ‘ 𝑋 ) ∧ 𝑧 ∈ ( 𝐽 ‘ 𝑌 ) ) ∧ ( 𝐹 = ( 𝑥 ( +g ‘ 𝑉 ) 𝑧 ) ∧ 𝑆 = 𝑂 ) ) ↔ ( ( ( 𝑥 ∈ ( 𝐽 ‘ 𝑋 ) ∧ 𝑧 ∈ ( 𝐽 ‘ 𝑌 ) ) ∧ 𝐹 = ( 𝑥 ( +g ‘ 𝑉 ) 𝑧 ) ) ∧ 𝑆 = 𝑂 ) )
97 96 2exbii ⊢ ( ∃ 𝑥 ∃ 𝑧 ( ( 𝑥 ∈ ( 𝐽 ‘ 𝑋 ) ∧ 𝑧 ∈ ( 𝐽 ‘ 𝑌 ) ) ∧ ( 𝐹 = ( 𝑥 ( +g ‘ 𝑉 ) 𝑧 ) ∧ 𝑆 = 𝑂 ) ) ↔ ∃ 𝑥 ∃ 𝑧 ( ( ( 𝑥 ∈ ( 𝐽 ‘ 𝑋 ) ∧ 𝑧 ∈ ( 𝐽 ‘ 𝑌 ) ) ∧ 𝐹 = ( 𝑥 ( +g ‘ 𝑉 ) 𝑧 ) ) ∧ 𝑆 = 𝑂 ) )
98 19.41vv ⊢ ( ∃ 𝑥 ∃ 𝑧 ( ( ( 𝑥 ∈ ( 𝐽 ‘ 𝑋 ) ∧ 𝑧 ∈ ( 𝐽 ‘ 𝑌 ) ) ∧ 𝐹 = ( 𝑥 ( +g ‘ 𝑉 ) 𝑧 ) ) ∧ 𝑆 = 𝑂 ) ↔ ( ∃ 𝑥 ∃ 𝑧 ( ( 𝑥 ∈ ( 𝐽 ‘ 𝑋 ) ∧ 𝑧 ∈ ( 𝐽 ‘ 𝑌 ) ) ∧ 𝐹 = ( 𝑥 ( +g ‘ 𝑉 ) 𝑧 ) ) ∧ 𝑆 = 𝑂 ) )
99 97 98 bitri ⊢ ( ∃ 𝑥 ∃ 𝑧 ( ( 𝑥 ∈ ( 𝐽 ‘ 𝑋 ) ∧ 𝑧 ∈ ( 𝐽 ‘ 𝑌 ) ) ∧ ( 𝐹 = ( 𝑥 ( +g ‘ 𝑉 ) 𝑧 ) ∧ 𝑆 = 𝑂 ) ) ↔ ( ∃ 𝑥 ∃ 𝑧 ( ( 𝑥 ∈ ( 𝐽 ‘ 𝑋 ) ∧ 𝑧 ∈ ( 𝐽 ‘ 𝑌 ) ) ∧ 𝐹 = ( 𝑥 ( +g ‘ 𝑉 ) 𝑧 ) ) ∧ 𝑆 = 𝑂 ) )
100 3 6 dvalvec ⊢ ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) → 𝑉 ∈ LVec )
101 lveclmod ⊢ ( 𝑉 ∈ LVec → 𝑉 ∈ LMod )
102 eqid ⊢ ( LSubSp ‘ 𝑉 ) = ( LSubSp ‘ 𝑉 )
103 102 lsssssubg ⊢ ( 𝑉 ∈ LMod → ( LSubSp ‘ 𝑉 ) ⊆ ( SubGrp ‘ 𝑉 ) )
104 12 100 101 103 4syl ⊢ ( 𝜑 → ( LSubSp ‘ 𝑉 ) ⊆ ( SubGrp ‘ 𝑉 ) )
105 1 2 3 6 10 102 dialss ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑋 ≤ 𝑊 ) ) → ( 𝐽 ‘ 𝑋 ) ∈ ( LSubSp ‘ 𝑉 ) )
106 12 13 105 syl2anc ⊢ ( 𝜑 → ( 𝐽 ‘ 𝑋 ) ∈ ( LSubSp ‘ 𝑉 ) )
107 104 106 sseldd ⊢ ( 𝜑 → ( 𝐽 ‘ 𝑋 ) ∈ ( SubGrp ‘ 𝑉 ) )
108 1 2 3 6 10 102 dialss ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑌 ∈ 𝐵 ∧ 𝑌 ≤ 𝑊 ) ) → ( 𝐽 ‘ 𝑌 ) ∈ ( LSubSp ‘ 𝑉 ) )
109 12 14 108 syl2anc ⊢ ( 𝜑 → ( 𝐽 ‘ 𝑌 ) ∈ ( LSubSp ‘ 𝑉 ) )
110 104 109 sseldd ⊢ ( 𝜑 → ( 𝐽 ‘ 𝑌 ) ∈ ( SubGrp ‘ 𝑉 ) )
111 73 8 lsmelval ⊢ ( ( ( 𝐽 ‘ 𝑋 ) ∈ ( SubGrp ‘ 𝑉 ) ∧ ( 𝐽 ‘ 𝑌 ) ∈ ( SubGrp ‘ 𝑉 ) ) → ( 𝐹 ∈ ( ( 𝐽 ‘ 𝑋 ) ⊕ ( 𝐽 ‘ 𝑌 ) ) ↔ ∃ 𝑥 ∈ ( 𝐽 ‘ 𝑋 ) ∃ 𝑧 ∈ ( 𝐽 ‘ 𝑌 ) 𝐹 = ( 𝑥 ( +g ‘ 𝑉 ) 𝑧 ) ) )
112 107 110 111 syl2anc ⊢ ( 𝜑 → ( 𝐹 ∈ ( ( 𝐽 ‘ 𝑋 ) ⊕ ( 𝐽 ‘ 𝑌 ) ) ↔ ∃ 𝑥 ∈ ( 𝐽 ‘ 𝑋 ) ∃ 𝑧 ∈ ( 𝐽 ‘ 𝑌 ) 𝐹 = ( 𝑥 ( +g ‘ 𝑉 ) 𝑧 ) ) )
113 r2ex ⊢ ( ∃ 𝑥 ∈ ( 𝐽 ‘ 𝑋 ) ∃ 𝑧 ∈ ( 𝐽 ‘ 𝑌 ) 𝐹 = ( 𝑥 ( +g ‘ 𝑉 ) 𝑧 ) ↔ ∃ 𝑥 ∃ 𝑧 ( ( 𝑥 ∈ ( 𝐽 ‘ 𝑋 ) ∧ 𝑧 ∈ ( 𝐽 ‘ 𝑌 ) ) ∧ 𝐹 = ( 𝑥 ( +g ‘ 𝑉 ) 𝑧 ) ) )
114 112 113 bitrdi ⊢ ( 𝜑 → ( 𝐹 ∈ ( ( 𝐽 ‘ 𝑋 ) ⊕ ( 𝐽 ‘ 𝑌 ) ) ↔ ∃ 𝑥 ∃ 𝑧 ( ( 𝑥 ∈ ( 𝐽 ‘ 𝑋 ) ∧ 𝑧 ∈ ( 𝐽 ‘ 𝑌 ) ) ∧ 𝐹 = ( 𝑥 ( +g ‘ 𝑉 ) 𝑧 ) ) ) )
115 114 anbi1d ⊢ ( 𝜑 → ( ( 𝐹 ∈ ( ( 𝐽 ‘ 𝑋 ) ⊕ ( 𝐽 ‘ 𝑌 ) ) ∧ 𝑆 = 𝑂 ) ↔ ( ∃ 𝑥 ∃ 𝑧 ( ( 𝑥 ∈ ( 𝐽 ‘ 𝑋 ) ∧ 𝑧 ∈ ( 𝐽 ‘ 𝑌 ) ) ∧ 𝐹 = ( 𝑥 ( +g ‘ 𝑉 ) 𝑧 ) ) ∧ 𝑆 = 𝑂 ) ) )
116 115 bicomd ⊢ ( 𝜑 → ( ( ∃ 𝑥 ∃ 𝑧 ( ( 𝑥 ∈ ( 𝐽 ‘ 𝑋 ) ∧ 𝑧 ∈ ( 𝐽 ‘ 𝑌 ) ) ∧ 𝐹 = ( 𝑥 ( +g ‘ 𝑉 ) 𝑧 ) ) ∧ 𝑆 = 𝑂 ) ↔ ( 𝐹 ∈ ( ( 𝐽 ‘ 𝑋 ) ⊕ ( 𝐽 ‘ 𝑌 ) ) ∧ 𝑆 = 𝑂 ) ) )
117 99 116 syl5bb ⊢ ( 𝜑 → ( ∃ 𝑥 ∃ 𝑧 ( ( 𝑥 ∈ ( 𝐽 ‘ 𝑋 ) ∧ 𝑧 ∈ ( 𝐽 ‘ 𝑌 ) ) ∧ ( 𝐹 = ( 𝑥 ( +g ‘ 𝑉 ) 𝑧 ) ∧ 𝑆 = 𝑂 ) ) ↔ ( 𝐹 ∈ ( ( 𝐽 ‘ 𝑋 ) ⊕ ( 𝐽 ‘ 𝑌 ) ) ∧ 𝑆 = 𝑂 ) ) )
118 22 94 117 3bitrd ⊢ ( 𝜑 → ( ⟨ 𝐹 , 𝑆 ⟩ ∈ ( ( 𝐼 ‘ 𝑋 ) ✚ ( 𝐼 ‘ 𝑌 ) ) ↔ ( 𝐹 ∈ ( ( 𝐽 ‘ 𝑋 ) ⊕ ( 𝐽 ‘ 𝑌 ) ) ∧ 𝑆 = 𝑂 ) ) )