This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem dvhopellsm

Description: Ordered pair membership in a subspace sum. (Contributed by NM, 12-Mar-2014)

Ref Expression
Hypotheses dvhopellsm.h ⊢ 𝐻 = ( LHyp ‘ 𝐾 )
dvhopellsm.u ⊢ 𝑈 = ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 )
dvhopellsm.a ⊢ + = ( +g ‘ 𝑈 )
dvhopellsm.s ⊢ 𝑆 = ( LSubSp ‘ 𝑈 )
dvhopellsm.p ⊢ ⊕ = ( LSSum ‘ 𝑈 )
Assertion dvhopellsm ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑋 ∈ 𝑆 ∧ 𝑌 ∈ 𝑆 ) → ( ⟨ 𝐹 , 𝑇 ⟩ ∈ ( 𝑋 ⊕ 𝑌 ) ↔ ∃ 𝑥 ∃ 𝑦 ∃ 𝑧 ∃ 𝑤 ( ( ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝑋 ∧ ⟨ 𝑧 , 𝑤 ⟩ ∈ 𝑌 ) ∧ ⟨ 𝐹 , 𝑇 ⟩ = ( ⟨ 𝑥 , 𝑦 ⟩ + ⟨ 𝑧 , 𝑤 ⟩ ) ) ) )

Proof

Step Hyp Ref Expression
1 dvhopellsm.h ⊢ 𝐻 = ( LHyp ‘ 𝐾 )
2 dvhopellsm.u ⊢ 𝑈 = ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 )
3 dvhopellsm.a ⊢ + = ( +g ‘ 𝑈 )
4 dvhopellsm.s ⊢ 𝑆 = ( LSubSp ‘ 𝑈 )
5 dvhopellsm.p ⊢ ⊕ = ( LSSum ‘ 𝑈 )
6 id ⊢ ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) → ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) )
7 1 2 6 dvhlmod ⊢ ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) → 𝑈 ∈ LMod )
8 7 3ad2ant1 ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑋 ∈ 𝑆 ∧ 𝑌 ∈ 𝑆 ) → 𝑈 ∈ LMod )
9 4 lsssssubg ⊢ ( 𝑈 ∈ LMod → 𝑆 ⊆ ( SubGrp ‘ 𝑈 ) )
10 8 9 syl ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑋 ∈ 𝑆 ∧ 𝑌 ∈ 𝑆 ) → 𝑆 ⊆ ( SubGrp ‘ 𝑈 ) )
11 simp2 ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑋 ∈ 𝑆 ∧ 𝑌 ∈ 𝑆 ) → 𝑋 ∈ 𝑆 )
12 10 11 sseldd ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑋 ∈ 𝑆 ∧ 𝑌 ∈ 𝑆 ) → 𝑋 ∈ ( SubGrp ‘ 𝑈 ) )
13 simp3 ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑋 ∈ 𝑆 ∧ 𝑌 ∈ 𝑆 ) → 𝑌 ∈ 𝑆 )
14 10 13 sseldd ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑋 ∈ 𝑆 ∧ 𝑌 ∈ 𝑆 ) → 𝑌 ∈ ( SubGrp ‘ 𝑈 ) )
15 3 5 lsmelval ⊢ ( ( 𝑋 ∈ ( SubGrp ‘ 𝑈 ) ∧ 𝑌 ∈ ( SubGrp ‘ 𝑈 ) ) → ( ⟨ 𝐹 , 𝑇 ⟩ ∈ ( 𝑋 ⊕ 𝑌 ) ↔ ∃ 𝑢 ∈ 𝑋 ∃ 𝑣 ∈ 𝑌 ⟨ 𝐹 , 𝑇 ⟩ = ( 𝑢 + 𝑣 ) ) )
16 12 14 15 syl2anc ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑋 ∈ 𝑆 ∧ 𝑌 ∈ 𝑆 ) → ( ⟨ 𝐹 , 𝑇 ⟩ ∈ ( 𝑋 ⊕ 𝑌 ) ↔ ∃ 𝑢 ∈ 𝑋 ∃ 𝑣 ∈ 𝑌 ⟨ 𝐹 , 𝑇 ⟩ = ( 𝑢 + 𝑣 ) ) )
17 eqid ⊢ ( Base ‘ 𝑈 ) = ( Base ‘ 𝑈 )
18 17 4 lssss ⊢ ( 𝑌 ∈ 𝑆 → 𝑌 ⊆ ( Base ‘ 𝑈 ) )
19 18 3ad2ant3 ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑋 ∈ 𝑆 ∧ 𝑌 ∈ 𝑆 ) → 𝑌 ⊆ ( Base ‘ 𝑈 ) )
20 eqid ⊢ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) = ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 )
21 eqid ⊢ ( ( TEndo ‘ 𝐾 ) ‘ 𝑊 ) = ( ( TEndo ‘ 𝐾 ) ‘ 𝑊 )
22 1 20 21 2 17 dvhvbase ⊢ ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) → ( Base ‘ 𝑈 ) = ( ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) × ( ( TEndo ‘ 𝐾 ) ‘ 𝑊 ) ) )
23 22 3ad2ant1 ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑋 ∈ 𝑆 ∧ 𝑌 ∈ 𝑆 ) → ( Base ‘ 𝑈 ) = ( ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) × ( ( TEndo ‘ 𝐾 ) ‘ 𝑊 ) ) )
24 19 23 sseqtrd ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑋 ∈ 𝑆 ∧ 𝑌 ∈ 𝑆 ) → 𝑌 ⊆ ( ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) × ( ( TEndo ‘ 𝐾 ) ‘ 𝑊 ) ) )
25 relxp ⊢ Rel ( ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) × ( ( TEndo ‘ 𝐾 ) ‘ 𝑊 ) )
26 relss ⊢ ( 𝑌 ⊆ ( ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) × ( ( TEndo ‘ 𝐾 ) ‘ 𝑊 ) ) → ( Rel ( ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) × ( ( TEndo ‘ 𝐾 ) ‘ 𝑊 ) ) → Rel 𝑌 ) )
27 24 25 26 mpisyl ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑋 ∈ 𝑆 ∧ 𝑌 ∈ 𝑆 ) → Rel 𝑌 )
28 oveq2 ⊢ ( 𝑣 = ⟨ 𝑧 , 𝑤 ⟩ → ( 𝑢 + 𝑣 ) = ( 𝑢 + ⟨ 𝑧 , 𝑤 ⟩ ) )
29 28 eqeq2d ⊢ ( 𝑣 = ⟨ 𝑧 , 𝑤 ⟩ → ( ⟨ 𝐹 , 𝑇 ⟩ = ( 𝑢 + 𝑣 ) ↔ ⟨ 𝐹 , 𝑇 ⟩ = ( 𝑢 + ⟨ 𝑧 , 𝑤 ⟩ ) ) )
30 29 exopxfr2 ⊢ ( Rel 𝑌 → ( ∃ 𝑣 ∈ 𝑌 ⟨ 𝐹 , 𝑇 ⟩ = ( 𝑢 + 𝑣 ) ↔ ∃ 𝑧 ∃ 𝑤 ( ⟨ 𝑧 , 𝑤 ⟩ ∈ 𝑌 ∧ ⟨ 𝐹 , 𝑇 ⟩ = ( 𝑢 + ⟨ 𝑧 , 𝑤 ⟩ ) ) ) )
31 27 30 syl ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑋 ∈ 𝑆 ∧ 𝑌 ∈ 𝑆 ) → ( ∃ 𝑣 ∈ 𝑌 ⟨ 𝐹 , 𝑇 ⟩ = ( 𝑢 + 𝑣 ) ↔ ∃ 𝑧 ∃ 𝑤 ( ⟨ 𝑧 , 𝑤 ⟩ ∈ 𝑌 ∧ ⟨ 𝐹 , 𝑇 ⟩ = ( 𝑢 + ⟨ 𝑧 , 𝑤 ⟩ ) ) ) )
32 31 rexbidv ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑋 ∈ 𝑆 ∧ 𝑌 ∈ 𝑆 ) → ( ∃ 𝑢 ∈ 𝑋 ∃ 𝑣 ∈ 𝑌 ⟨ 𝐹 , 𝑇 ⟩ = ( 𝑢 + 𝑣 ) ↔ ∃ 𝑢 ∈ 𝑋 ∃ 𝑧 ∃ 𝑤 ( ⟨ 𝑧 , 𝑤 ⟩ ∈ 𝑌 ∧ ⟨ 𝐹 , 𝑇 ⟩ = ( 𝑢 + ⟨ 𝑧 , 𝑤 ⟩ ) ) ) )
33 17 4 lssss ⊢ ( 𝑋 ∈ 𝑆 → 𝑋 ⊆ ( Base ‘ 𝑈 ) )
34 33 3ad2ant2 ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑋 ∈ 𝑆 ∧ 𝑌 ∈ 𝑆 ) → 𝑋 ⊆ ( Base ‘ 𝑈 ) )
35 34 23 sseqtrd ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑋 ∈ 𝑆 ∧ 𝑌 ∈ 𝑆 ) → 𝑋 ⊆ ( ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) × ( ( TEndo ‘ 𝐾 ) ‘ 𝑊 ) ) )
36 relss ⊢ ( 𝑋 ⊆ ( ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) × ( ( TEndo ‘ 𝐾 ) ‘ 𝑊 ) ) → ( Rel ( ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) × ( ( TEndo ‘ 𝐾 ) ‘ 𝑊 ) ) → Rel 𝑋 ) )
37 35 25 36 mpisyl ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑋 ∈ 𝑆 ∧ 𝑌 ∈ 𝑆 ) → Rel 𝑋 )
38 oveq1 ⊢ ( 𝑢 = ⟨ 𝑥 , 𝑦 ⟩ → ( 𝑢 + ⟨ 𝑧 , 𝑤 ⟩ ) = ( ⟨ 𝑥 , 𝑦 ⟩ + ⟨ 𝑧 , 𝑤 ⟩ ) )
39 38 eqeq2d ⊢ ( 𝑢 = ⟨ 𝑥 , 𝑦 ⟩ → ( ⟨ 𝐹 , 𝑇 ⟩ = ( 𝑢 + ⟨ 𝑧 , 𝑤 ⟩ ) ↔ ⟨ 𝐹 , 𝑇 ⟩ = ( ⟨ 𝑥 , 𝑦 ⟩ + ⟨ 𝑧 , 𝑤 ⟩ ) ) )
40 39 anbi2d ⊢ ( 𝑢 = ⟨ 𝑥 , 𝑦 ⟩ → ( ( ⟨ 𝑧 , 𝑤 ⟩ ∈ 𝑌 ∧ ⟨ 𝐹 , 𝑇 ⟩ = ( 𝑢 + ⟨ 𝑧 , 𝑤 ⟩ ) ) ↔ ( ⟨ 𝑧 , 𝑤 ⟩ ∈ 𝑌 ∧ ⟨ 𝐹 , 𝑇 ⟩ = ( ⟨ 𝑥 , 𝑦 ⟩ + ⟨ 𝑧 , 𝑤 ⟩ ) ) ) )
41 40 2exbidv ⊢ ( 𝑢 = ⟨ 𝑥 , 𝑦 ⟩ → ( ∃ 𝑧 ∃ 𝑤 ( ⟨ 𝑧 , 𝑤 ⟩ ∈ 𝑌 ∧ ⟨ 𝐹 , 𝑇 ⟩ = ( 𝑢 + ⟨ 𝑧 , 𝑤 ⟩ ) ) ↔ ∃ 𝑧 ∃ 𝑤 ( ⟨ 𝑧 , 𝑤 ⟩ ∈ 𝑌 ∧ ⟨ 𝐹 , 𝑇 ⟩ = ( ⟨ 𝑥 , 𝑦 ⟩ + ⟨ 𝑧 , 𝑤 ⟩ ) ) ) )
42 41 exopxfr2 ⊢ ( Rel 𝑋 → ( ∃ 𝑢 ∈ 𝑋 ∃ 𝑧 ∃ 𝑤 ( ⟨ 𝑧 , 𝑤 ⟩ ∈ 𝑌 ∧ ⟨ 𝐹 , 𝑇 ⟩ = ( 𝑢 + ⟨ 𝑧 , 𝑤 ⟩ ) ) ↔ ∃ 𝑥 ∃ 𝑦 ( ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝑋 ∧ ∃ 𝑧 ∃ 𝑤 ( ⟨ 𝑧 , 𝑤 ⟩ ∈ 𝑌 ∧ ⟨ 𝐹 , 𝑇 ⟩ = ( ⟨ 𝑥 , 𝑦 ⟩ + ⟨ 𝑧 , 𝑤 ⟩ ) ) ) ) )
43 37 42 syl ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑋 ∈ 𝑆 ∧ 𝑌 ∈ 𝑆 ) → ( ∃ 𝑢 ∈ 𝑋 ∃ 𝑧 ∃ 𝑤 ( ⟨ 𝑧 , 𝑤 ⟩ ∈ 𝑌 ∧ ⟨ 𝐹 , 𝑇 ⟩ = ( 𝑢 + ⟨ 𝑧 , 𝑤 ⟩ ) ) ↔ ∃ 𝑥 ∃ 𝑦 ( ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝑋 ∧ ∃ 𝑧 ∃ 𝑤 ( ⟨ 𝑧 , 𝑤 ⟩ ∈ 𝑌 ∧ ⟨ 𝐹 , 𝑇 ⟩ = ( ⟨ 𝑥 , 𝑦 ⟩ + ⟨ 𝑧 , 𝑤 ⟩ ) ) ) ) )
44 19.42vv ⊢ ( ∃ 𝑧 ∃ 𝑤 ( ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝑋 ∧ ( ⟨ 𝑧 , 𝑤 ⟩ ∈ 𝑌 ∧ ⟨ 𝐹 , 𝑇 ⟩ = ( ⟨ 𝑥 , 𝑦 ⟩ + ⟨ 𝑧 , 𝑤 ⟩ ) ) ) ↔ ( ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝑋 ∧ ∃ 𝑧 ∃ 𝑤 ( ⟨ 𝑧 , 𝑤 ⟩ ∈ 𝑌 ∧ ⟨ 𝐹 , 𝑇 ⟩ = ( ⟨ 𝑥 , 𝑦 ⟩ + ⟨ 𝑧 , 𝑤 ⟩ ) ) ) )
45 anass ⊢ ( ( ( ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝑋 ∧ ⟨ 𝑧 , 𝑤 ⟩ ∈ 𝑌 ) ∧ ⟨ 𝐹 , 𝑇 ⟩ = ( ⟨ 𝑥 , 𝑦 ⟩ + ⟨ 𝑧 , 𝑤 ⟩ ) ) ↔ ( ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝑋 ∧ ( ⟨ 𝑧 , 𝑤 ⟩ ∈ 𝑌 ∧ ⟨ 𝐹 , 𝑇 ⟩ = ( ⟨ 𝑥 , 𝑦 ⟩ + ⟨ 𝑧 , 𝑤 ⟩ ) ) ) )
46 45 2exbii ⊢ ( ∃ 𝑧 ∃ 𝑤 ( ( ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝑋 ∧ ⟨ 𝑧 , 𝑤 ⟩ ∈ 𝑌 ) ∧ ⟨ 𝐹 , 𝑇 ⟩ = ( ⟨ 𝑥 , 𝑦 ⟩ + ⟨ 𝑧 , 𝑤 ⟩ ) ) ↔ ∃ 𝑧 ∃ 𝑤 ( ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝑋 ∧ ( ⟨ 𝑧 , 𝑤 ⟩ ∈ 𝑌 ∧ ⟨ 𝐹 , 𝑇 ⟩ = ( ⟨ 𝑥 , 𝑦 ⟩ + ⟨ 𝑧 , 𝑤 ⟩ ) ) ) )
47 46 bicomi ⊢ ( ∃ 𝑧 ∃ 𝑤 ( ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝑋 ∧ ( ⟨ 𝑧 , 𝑤 ⟩ ∈ 𝑌 ∧ ⟨ 𝐹 , 𝑇 ⟩ = ( ⟨ 𝑥 , 𝑦 ⟩ + ⟨ 𝑧 , 𝑤 ⟩ ) ) ) ↔ ∃ 𝑧 ∃ 𝑤 ( ( ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝑋 ∧ ⟨ 𝑧 , 𝑤 ⟩ ∈ 𝑌 ) ∧ ⟨ 𝐹 , 𝑇 ⟩ = ( ⟨ 𝑥 , 𝑦 ⟩ + ⟨ 𝑧 , 𝑤 ⟩ ) ) )
48 47 a1i ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑋 ∈ 𝑆 ∧ 𝑌 ∈ 𝑆 ) → ( ∃ 𝑧 ∃ 𝑤 ( ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝑋 ∧ ( ⟨ 𝑧 , 𝑤 ⟩ ∈ 𝑌 ∧ ⟨ 𝐹 , 𝑇 ⟩ = ( ⟨ 𝑥 , 𝑦 ⟩ + ⟨ 𝑧 , 𝑤 ⟩ ) ) ) ↔ ∃ 𝑧 ∃ 𝑤 ( ( ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝑋 ∧ ⟨ 𝑧 , 𝑤 ⟩ ∈ 𝑌 ) ∧ ⟨ 𝐹 , 𝑇 ⟩ = ( ⟨ 𝑥 , 𝑦 ⟩ + ⟨ 𝑧 , 𝑤 ⟩ ) ) ) )
49 44 48 bitr3id ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑋 ∈ 𝑆 ∧ 𝑌 ∈ 𝑆 ) → ( ( ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝑋 ∧ ∃ 𝑧 ∃ 𝑤 ( ⟨ 𝑧 , 𝑤 ⟩ ∈ 𝑌 ∧ ⟨ 𝐹 , 𝑇 ⟩ = ( ⟨ 𝑥 , 𝑦 ⟩ + ⟨ 𝑧 , 𝑤 ⟩ ) ) ) ↔ ∃ 𝑧 ∃ 𝑤 ( ( ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝑋 ∧ ⟨ 𝑧 , 𝑤 ⟩ ∈ 𝑌 ) ∧ ⟨ 𝐹 , 𝑇 ⟩ = ( ⟨ 𝑥 , 𝑦 ⟩ + ⟨ 𝑧 , 𝑤 ⟩ ) ) ) )
50 49 2exbidv ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑋 ∈ 𝑆 ∧ 𝑌 ∈ 𝑆 ) → ( ∃ 𝑥 ∃ 𝑦 ( ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝑋 ∧ ∃ 𝑧 ∃ 𝑤 ( ⟨ 𝑧 , 𝑤 ⟩ ∈ 𝑌 ∧ ⟨ 𝐹 , 𝑇 ⟩ = ( ⟨ 𝑥 , 𝑦 ⟩ + ⟨ 𝑧 , 𝑤 ⟩ ) ) ) ↔ ∃ 𝑥 ∃ 𝑦 ∃ 𝑧 ∃ 𝑤 ( ( ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝑋 ∧ ⟨ 𝑧 , 𝑤 ⟩ ∈ 𝑌 ) ∧ ⟨ 𝐹 , 𝑇 ⟩ = ( ⟨ 𝑥 , 𝑦 ⟩ + ⟨ 𝑧 , 𝑤 ⟩ ) ) ) )
51 43 50 bitrd ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑋 ∈ 𝑆 ∧ 𝑌 ∈ 𝑆 ) → ( ∃ 𝑢 ∈ 𝑋 ∃ 𝑧 ∃ 𝑤 ( ⟨ 𝑧 , 𝑤 ⟩ ∈ 𝑌 ∧ ⟨ 𝐹 , 𝑇 ⟩ = ( 𝑢 + ⟨ 𝑧 , 𝑤 ⟩ ) ) ↔ ∃ 𝑥 ∃ 𝑦 ∃ 𝑧 ∃ 𝑤 ( ( ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝑋 ∧ ⟨ 𝑧 , 𝑤 ⟩ ∈ 𝑌 ) ∧ ⟨ 𝐹 , 𝑇 ⟩ = ( ⟨ 𝑥 , 𝑦 ⟩ + ⟨ 𝑧 , 𝑤 ⟩ ) ) ) )
52 16 32 51 3bitrd ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑋 ∈ 𝑆 ∧ 𝑌 ∈ 𝑆 ) → ( ⟨ 𝐹 , 𝑇 ⟩ ∈ ( 𝑋 ⊕ 𝑌 ) ↔ ∃ 𝑥 ∃ 𝑦 ∃ 𝑧 ∃ 𝑤 ( ( ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝑋 ∧ ⟨ 𝑧 , 𝑤 ⟩ ∈ 𝑌 ) ∧ ⟨ 𝐹 , 𝑇 ⟩ = ( ⟨ 𝑥 , 𝑦 ⟩ + ⟨ 𝑧 , 𝑤 ⟩ ) ) ) )