Metamath Proof Explorer

Theorem lcfrlem23

Description: Lemma for lcfr . TODO: this proof was built from other proof pieces that may change N{ X , Y } into subspace sum and back unnecessarily, or similar things. (Contributed by NM, 1-Mar-2015)

Ref Expression
Hypotheses lcfrlem17.h ⊢ 𝐻 = ( LHyp ‘ 𝐾 )
lcfrlem17.o ⊢ ⊥ = ( ( ocH ‘ 𝐾 ) ‘ 𝑊 )
lcfrlem17.u ⊢ 𝑈 = ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 )
lcfrlem17.v ⊢ 𝑉 = ( Base ‘ 𝑈 )
lcfrlem17.p ⊢ + = ( +g ‘ 𝑈 )
lcfrlem17.z ⊢ 0 = ( 0g ‘ 𝑈 )
lcfrlem17.n ⊢ 𝑁 = ( LSpan ‘ 𝑈 )
lcfrlem17.a ⊢ 𝐴 = ( LSAtoms ‘ 𝑈 )
lcfrlem17.k ⊢ ( 𝜑 → ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) )
lcfrlem17.x ⊢ ( 𝜑 → 𝑋 ∈ ( 𝑉 ∖ { 0 } ) )
lcfrlem17.y ⊢ ( 𝜑 → 𝑌 ∈ ( 𝑉 ∖ { 0 } ) )
lcfrlem17.ne ⊢ ( 𝜑 → ( 𝑁 ‘ { 𝑋 } ) ≠ ( 𝑁 ‘ { 𝑌 } ) )
lcfrlem22.b ⊢ 𝐵 = ( ( 𝑁 ‘ { 𝑋 , 𝑌 } ) ∩ ( ⊥ ‘ { ( 𝑋 + 𝑌 ) } ) )
lcfrlem23.s ⊢ ⊕ = ( LSSum ‘ 𝑈 )
Assertion lcfrlem23 ( 𝜑 → ( ( ⊥ ‘ { 𝑋 , 𝑌 } ) ⊕ 𝐵 ) = ( ⊥ ‘ { ( 𝑋 + 𝑌 ) } ) )

Proof

Step Hyp Ref Expression
1 lcfrlem17.h ⊢ 𝐻 = ( LHyp ‘ 𝐾 )
2 lcfrlem17.o ⊢ ⊥ = ( ( ocH ‘ 𝐾 ) ‘ 𝑊 )
3 lcfrlem17.u ⊢ 𝑈 = ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 )
4 lcfrlem17.v ⊢ 𝑉 = ( Base ‘ 𝑈 )
5 lcfrlem17.p ⊢ + = ( +g ‘ 𝑈 )
6 lcfrlem17.z ⊢ 0 = ( 0g ‘ 𝑈 )
7 lcfrlem17.n ⊢ 𝑁 = ( LSpan ‘ 𝑈 )
8 lcfrlem17.a ⊢ 𝐴 = ( LSAtoms ‘ 𝑈 )
9 lcfrlem17.k ⊢ ( 𝜑 → ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) )
10 lcfrlem17.x ⊢ ( 𝜑 → 𝑋 ∈ ( 𝑉 ∖ { 0 } ) )
11 lcfrlem17.y ⊢ ( 𝜑 → 𝑌 ∈ ( 𝑉 ∖ { 0 } ) )
12 lcfrlem17.ne ⊢ ( 𝜑 → ( 𝑁 ‘ { 𝑋 } ) ≠ ( 𝑁 ‘ { 𝑌 } ) )
13 lcfrlem22.b ⊢ 𝐵 = ( ( 𝑁 ‘ { 𝑋 , 𝑌 } ) ∩ ( ⊥ ‘ { ( 𝑋 + 𝑌 ) } ) )
14 lcfrlem23.s ⊢ ⊕ = ( LSSum ‘ 𝑈 )
15 13 fveq2i ⊢ ( ⊥ ‘ 𝐵 ) = ( ⊥ ‘ ( ( 𝑁 ‘ { 𝑋 , 𝑌 } ) ∩ ( ⊥ ‘ { ( 𝑋 + 𝑌 ) } ) ) )
16 eqid ⊢ ( ( DIsoH ‘ 𝐾 ) ‘ 𝑊 ) = ( ( DIsoH ‘ 𝐾 ) ‘ 𝑊 )
17 eqid ⊢ ( ( joinH ‘ 𝐾 ) ‘ 𝑊 ) = ( ( joinH ‘ 𝐾 ) ‘ 𝑊 )
18 10 eldifad ⊢ ( 𝜑 → 𝑋 ∈ 𝑉 )
19 11 eldifad ⊢ ( 𝜑 → 𝑌 ∈ 𝑉 )
20 1 3 4 7 16 9 18 19 dihprrn ⊢ ( 𝜑 → ( 𝑁 ‘ { 𝑋 , 𝑌 } ) ∈ ran ( ( DIsoH ‘ 𝐾 ) ‘ 𝑊 ) )
21 1 3 9 dvhlmod ⊢ ( 𝜑 → 𝑈 ∈ LMod )
22 4 5 lmodvacl ⊢ ( ( 𝑈 ∈ LMod ∧ 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉 ) → ( 𝑋 + 𝑌 ) ∈ 𝑉 )
23 21 18 19 22 syl3anc ⊢ ( 𝜑 → ( 𝑋 + 𝑌 ) ∈ 𝑉 )
24 23 snssd ⊢ ( 𝜑 → { ( 𝑋 + 𝑌 ) } ⊆ 𝑉 )
25 1 16 3 4 2 dochcl ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ { ( 𝑋 + 𝑌 ) } ⊆ 𝑉 ) → ( ⊥ ‘ { ( 𝑋 + 𝑌 ) } ) ∈ ran ( ( DIsoH ‘ 𝐾 ) ‘ 𝑊 ) )
26 9 24 25 syl2anc ⊢ ( 𝜑 → ( ⊥ ‘ { ( 𝑋 + 𝑌 ) } ) ∈ ran ( ( DIsoH ‘ 𝐾 ) ‘ 𝑊 ) )
27 1 16 3 4 2 17 9 20 26 dochdmm1 ⊢ ( 𝜑 → ( ⊥ ‘ ( ( 𝑁 ‘ { 𝑋 , 𝑌 } ) ∩ ( ⊥ ‘ { ( 𝑋 + 𝑌 ) } ) ) ) = ( ( ⊥ ‘ ( 𝑁 ‘ { 𝑋 , 𝑌 } ) ) ( ( joinH ‘ 𝐾 ) ‘ 𝑊 ) ( ⊥ ‘ ( ⊥ ‘ { ( 𝑋 + 𝑌 ) } ) ) ) )
28 1 3 2 4 7 9 23 dochocsn ⊢ ( 𝜑 → ( ⊥ ‘ ( ⊥ ‘ { ( 𝑋 + 𝑌 ) } ) ) = ( 𝑁 ‘ { ( 𝑋 + 𝑌 ) } ) )
29 28 oveq2d ⊢ ( 𝜑 → ( ( ⊥ ‘ ( 𝑁 ‘ { 𝑋 , 𝑌 } ) ) ( ( joinH ‘ 𝐾 ) ‘ 𝑊 ) ( ⊥ ‘ ( ⊥ ‘ { ( 𝑋 + 𝑌 ) } ) ) ) = ( ( ⊥ ‘ ( 𝑁 ‘ { 𝑋 , 𝑌 } ) ) ( ( joinH ‘ 𝐾 ) ‘ 𝑊 ) ( 𝑁 ‘ { ( 𝑋 + 𝑌 ) } ) ) )
30 prssi ⊢ ( ( 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉 ) → { 𝑋 , 𝑌 } ⊆ 𝑉 )
31 18 19 30 syl2anc ⊢ ( 𝜑 → { 𝑋 , 𝑌 } ⊆ 𝑉 )
32 4 7 lspssv ⊢ ( ( 𝑈 ∈ LMod ∧ { 𝑋 , 𝑌 } ⊆ 𝑉 ) → ( 𝑁 ‘ { 𝑋 , 𝑌 } ) ⊆ 𝑉 )
33 21 31 32 syl2anc ⊢ ( 𝜑 → ( 𝑁 ‘ { 𝑋 , 𝑌 } ) ⊆ 𝑉 )
34 1 16 3 4 2 dochcl ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑁 ‘ { 𝑋 , 𝑌 } ) ⊆ 𝑉 ) → ( ⊥ ‘ ( 𝑁 ‘ { 𝑋 , 𝑌 } ) ) ∈ ran ( ( DIsoH ‘ 𝐾 ) ‘ 𝑊 ) )
35 9 33 34 syl2anc ⊢ ( 𝜑 → ( ⊥ ‘ ( 𝑁 ‘ { 𝑋 , 𝑌 } ) ) ∈ ran ( ( DIsoH ‘ 𝐾 ) ‘ 𝑊 ) )
36 1 3 4 14 7 16 17 9 35 23 dihjat1 ⊢ ( 𝜑 → ( ( ⊥ ‘ ( 𝑁 ‘ { 𝑋 , 𝑌 } ) ) ( ( joinH ‘ 𝐾 ) ‘ 𝑊 ) ( 𝑁 ‘ { ( 𝑋 + 𝑌 ) } ) ) = ( ( ⊥ ‘ ( 𝑁 ‘ { 𝑋 , 𝑌 } ) ) ⊕ ( 𝑁 ‘ { ( 𝑋 + 𝑌 ) } ) ) )
37 27 29 36 3eqtrd ⊢ ( 𝜑 → ( ⊥ ‘ ( ( 𝑁 ‘ { 𝑋 , 𝑌 } ) ∩ ( ⊥ ‘ { ( 𝑋 + 𝑌 ) } ) ) ) = ( ( ⊥ ‘ ( 𝑁 ‘ { 𝑋 , 𝑌 } ) ) ⊕ ( 𝑁 ‘ { ( 𝑋 + 𝑌 ) } ) ) )
38 15 37 eqtrid ⊢ ( 𝜑 → ( ⊥ ‘ 𝐵 ) = ( ( ⊥ ‘ ( 𝑁 ‘ { 𝑋 , 𝑌 } ) ) ⊕ ( 𝑁 ‘ { ( 𝑋 + 𝑌 ) } ) ) )
39 38 ineq2d ⊢ ( 𝜑 → ( ( ( 𝑁 ‘ { 𝑋 } ) ⊕ ( 𝑁 ‘ { 𝑌 } ) ) ∩ ( ⊥ ‘ 𝐵 ) ) = ( ( ( 𝑁 ‘ { 𝑋 } ) ⊕ ( 𝑁 ‘ { 𝑌 } ) ) ∩ ( ( ⊥ ‘ ( 𝑁 ‘ { 𝑋 , 𝑌 } ) ) ⊕ ( 𝑁 ‘ { ( 𝑋 + 𝑌 ) } ) ) ) )
40 eqid ⊢ ( LSubSp ‘ 𝑈 ) = ( LSubSp ‘ 𝑈 )
41 40 lsssssubg ⊢ ( 𝑈 ∈ LMod → ( LSubSp ‘ 𝑈 ) ⊆ ( SubGrp ‘ 𝑈 ) )
42 21 41 syl ⊢ ( 𝜑 → ( LSubSp ‘ 𝑈 ) ⊆ ( SubGrp ‘ 𝑈 ) )
43 4 40 7 lspsncl ⊢ ( ( 𝑈 ∈ LMod ∧ 𝑋 ∈ 𝑉 ) → ( 𝑁 ‘ { 𝑋 } ) ∈ ( LSubSp ‘ 𝑈 ) )
44 21 18 43 syl2anc ⊢ ( 𝜑 → ( 𝑁 ‘ { 𝑋 } ) ∈ ( LSubSp ‘ 𝑈 ) )
45 4 40 7 lspsncl ⊢ ( ( 𝑈 ∈ LMod ∧ 𝑌 ∈ 𝑉 ) → ( 𝑁 ‘ { 𝑌 } ) ∈ ( LSubSp ‘ 𝑈 ) )
46 21 19 45 syl2anc ⊢ ( 𝜑 → ( 𝑁 ‘ { 𝑌 } ) ∈ ( LSubSp ‘ 𝑈 ) )
47 40 14 lsmcl ⊢ ( ( 𝑈 ∈ LMod ∧ ( 𝑁 ‘ { 𝑋 } ) ∈ ( LSubSp ‘ 𝑈 ) ∧ ( 𝑁 ‘ { 𝑌 } ) ∈ ( LSubSp ‘ 𝑈 ) ) → ( ( 𝑁 ‘ { 𝑋 } ) ⊕ ( 𝑁 ‘ { 𝑌 } ) ) ∈ ( LSubSp ‘ 𝑈 ) )
48 21 44 46 47 syl3anc ⊢ ( 𝜑 → ( ( 𝑁 ‘ { 𝑋 } ) ⊕ ( 𝑁 ‘ { 𝑌 } ) ) ∈ ( LSubSp ‘ 𝑈 ) )
49 42 48 sseldd ⊢ ( 𝜑 → ( ( 𝑁 ‘ { 𝑋 } ) ⊕ ( 𝑁 ‘ { 𝑌 } ) ) ∈ ( SubGrp ‘ 𝑈 ) )
50 1 3 4 40 2 dochlss ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑁 ‘ { 𝑋 , 𝑌 } ) ⊆ 𝑉 ) → ( ⊥ ‘ ( 𝑁 ‘ { 𝑋 , 𝑌 } ) ) ∈ ( LSubSp ‘ 𝑈 ) )
51 9 33 50 syl2anc ⊢ ( 𝜑 → ( ⊥ ‘ ( 𝑁 ‘ { 𝑋 , 𝑌 } ) ) ∈ ( LSubSp ‘ 𝑈 ) )
52 42 51 sseldd ⊢ ( 𝜑 → ( ⊥ ‘ ( 𝑁 ‘ { 𝑋 , 𝑌 } ) ) ∈ ( SubGrp ‘ 𝑈 ) )
53 4 40 7 lspsncl ⊢ ( ( 𝑈 ∈ LMod ∧ ( 𝑋 + 𝑌 ) ∈ 𝑉 ) → ( 𝑁 ‘ { ( 𝑋 + 𝑌 ) } ) ∈ ( LSubSp ‘ 𝑈 ) )
54 21 23 53 syl2anc ⊢ ( 𝜑 → ( 𝑁 ‘ { ( 𝑋 + 𝑌 ) } ) ∈ ( LSubSp ‘ 𝑈 ) )
55 42 54 sseldd ⊢ ( 𝜑 → ( 𝑁 ‘ { ( 𝑋 + 𝑌 ) } ) ∈ ( SubGrp ‘ 𝑈 ) )
56 4 5 7 14 lspsntri ⊢ ( ( 𝑈 ∈ LMod ∧ 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉 ) → ( 𝑁 ‘ { ( 𝑋 + 𝑌 ) } ) ⊆ ( ( 𝑁 ‘ { 𝑋 } ) ⊕ ( 𝑁 ‘ { 𝑌 } ) ) )
57 21 18 19 56 syl3anc ⊢ ( 𝜑 → ( 𝑁 ‘ { ( 𝑋 + 𝑌 ) } ) ⊆ ( ( 𝑁 ‘ { 𝑋 } ) ⊕ ( 𝑁 ‘ { 𝑌 } ) ) )
58 14 lsmmod2 ⊢ ( ( ( ( ( 𝑁 ‘ { 𝑋 } ) ⊕ ( 𝑁 ‘ { 𝑌 } ) ) ∈ ( SubGrp ‘ 𝑈 ) ∧ ( ⊥ ‘ ( 𝑁 ‘ { 𝑋 , 𝑌 } ) ) ∈ ( SubGrp ‘ 𝑈 ) ∧ ( 𝑁 ‘ { ( 𝑋 + 𝑌 ) } ) ∈ ( SubGrp ‘ 𝑈 ) ) ∧ ( 𝑁 ‘ { ( 𝑋 + 𝑌 ) } ) ⊆ ( ( 𝑁 ‘ { 𝑋 } ) ⊕ ( 𝑁 ‘ { 𝑌 } ) ) ) → ( ( ( 𝑁 ‘ { 𝑋 } ) ⊕ ( 𝑁 ‘ { 𝑌 } ) ) ∩ ( ( ⊥ ‘ ( 𝑁 ‘ { 𝑋 , 𝑌 } ) ) ⊕ ( 𝑁 ‘ { ( 𝑋 + 𝑌 ) } ) ) ) = ( ( ( ( 𝑁 ‘ { 𝑋 } ) ⊕ ( 𝑁 ‘ { 𝑌 } ) ) ∩ ( ⊥ ‘ ( 𝑁 ‘ { 𝑋 , 𝑌 } ) ) ) ⊕ ( 𝑁 ‘ { ( 𝑋 + 𝑌 ) } ) ) )
59 49 52 55 57 58 syl31anc ⊢ ( 𝜑 → ( ( ( 𝑁 ‘ { 𝑋 } ) ⊕ ( 𝑁 ‘ { 𝑌 } ) ) ∩ ( ( ⊥ ‘ ( 𝑁 ‘ { 𝑋 , 𝑌 } ) ) ⊕ ( 𝑁 ‘ { ( 𝑋 + 𝑌 ) } ) ) ) = ( ( ( ( 𝑁 ‘ { 𝑋 } ) ⊕ ( 𝑁 ‘ { 𝑌 } ) ) ∩ ( ⊥ ‘ ( 𝑁 ‘ { 𝑋 , 𝑌 } ) ) ) ⊕ ( 𝑁 ‘ { ( 𝑋 + 𝑌 ) } ) ) )
60 4 7 14 21 18 19 lsmpr ⊢ ( 𝜑 → ( 𝑁 ‘ { 𝑋 , 𝑌 } ) = ( ( 𝑁 ‘ { 𝑋 } ) ⊕ ( 𝑁 ‘ { 𝑌 } ) ) )
61 60 ineq1d ⊢ ( 𝜑 → ( ( 𝑁 ‘ { 𝑋 , 𝑌 } ) ∩ ( ⊥ ‘ ( 𝑁 ‘ { 𝑋 , 𝑌 } ) ) ) = ( ( ( 𝑁 ‘ { 𝑋 } ) ⊕ ( 𝑁 ‘ { 𝑌 } ) ) ∩ ( ⊥ ‘ ( 𝑁 ‘ { 𝑋 , 𝑌 } ) ) ) )
62 4 40 7 21 18 19 lspprcl ⊢ ( 𝜑 → ( 𝑁 ‘ { 𝑋 , 𝑌 } ) ∈ ( LSubSp ‘ 𝑈 ) )
63 1 3 40 6 2 dochnoncon ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑁 ‘ { 𝑋 , 𝑌 } ) ∈ ( LSubSp ‘ 𝑈 ) ) → ( ( 𝑁 ‘ { 𝑋 , 𝑌 } ) ∩ ( ⊥ ‘ ( 𝑁 ‘ { 𝑋 , 𝑌 } ) ) ) = { 0 } )
64 9 62 63 syl2anc ⊢ ( 𝜑 → ( ( 𝑁 ‘ { 𝑋 , 𝑌 } ) ∩ ( ⊥ ‘ ( 𝑁 ‘ { 𝑋 , 𝑌 } ) ) ) = { 0 } )
65 61 64 eqtr3d ⊢ ( 𝜑 → ( ( ( 𝑁 ‘ { 𝑋 } ) ⊕ ( 𝑁 ‘ { 𝑌 } ) ) ∩ ( ⊥ ‘ ( 𝑁 ‘ { 𝑋 , 𝑌 } ) ) ) = { 0 } )
66 65 oveq1d ⊢ ( 𝜑 → ( ( ( ( 𝑁 ‘ { 𝑋 } ) ⊕ ( 𝑁 ‘ { 𝑌 } ) ) ∩ ( ⊥ ‘ ( 𝑁 ‘ { 𝑋 , 𝑌 } ) ) ) ⊕ ( 𝑁 ‘ { ( 𝑋 + 𝑌 ) } ) ) = ( { 0 } ⊕ ( 𝑁 ‘ { ( 𝑋 + 𝑌 ) } ) ) )
67 6 14 lsm02 ⊢ ( ( 𝑁 ‘ { ( 𝑋 + 𝑌 ) } ) ∈ ( SubGrp ‘ 𝑈 ) → ( { 0 } ⊕ ( 𝑁 ‘ { ( 𝑋 + 𝑌 ) } ) ) = ( 𝑁 ‘ { ( 𝑋 + 𝑌 ) } ) )
68 55 67 syl ⊢ ( 𝜑 → ( { 0 } ⊕ ( 𝑁 ‘ { ( 𝑋 + 𝑌 ) } ) ) = ( 𝑁 ‘ { ( 𝑋 + 𝑌 ) } ) )
69 66 68 eqtrd ⊢ ( 𝜑 → ( ( ( ( 𝑁 ‘ { 𝑋 } ) ⊕ ( 𝑁 ‘ { 𝑌 } ) ) ∩ ( ⊥ ‘ ( 𝑁 ‘ { 𝑋 , 𝑌 } ) ) ) ⊕ ( 𝑁 ‘ { ( 𝑋 + 𝑌 ) } ) ) = ( 𝑁 ‘ { ( 𝑋 + 𝑌 ) } ) )
70 39 59 69 3eqtrd ⊢ ( 𝜑 → ( ( ( 𝑁 ‘ { 𝑋 } ) ⊕ ( 𝑁 ‘ { 𝑌 } ) ) ∩ ( ⊥ ‘ 𝐵 ) ) = ( 𝑁 ‘ { ( 𝑋 + 𝑌 ) } ) )
71 70 fveq2d ⊢ ( 𝜑 → ( ⊥ ‘ ( ( ( 𝑁 ‘ { 𝑋 } ) ⊕ ( 𝑁 ‘ { 𝑌 } ) ) ∩ ( ⊥ ‘ 𝐵 ) ) ) = ( ⊥ ‘ ( 𝑁 ‘ { ( 𝑋 + 𝑌 ) } ) ) )
72 1 3 4 14 7 16 9 18 19 dihsmsnrn ⊢ ( 𝜑 → ( ( 𝑁 ‘ { 𝑋 } ) ⊕ ( 𝑁 ‘ { 𝑌 } ) ) ∈ ran ( ( DIsoH ‘ 𝐾 ) ‘ 𝑊 ) )
73 1 2 3 4 5 6 7 8 9 10 11 12 13 lcfrlem22 ⊢ ( 𝜑 → 𝐵 ∈ 𝐴 )
74 4 8 21 73 lsatssv ⊢ ( 𝜑 → 𝐵 ⊆ 𝑉 )
75 1 16 3 4 2 dochcl ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐵 ⊆ 𝑉 ) → ( ⊥ ‘ 𝐵 ) ∈ ran ( ( DIsoH ‘ 𝐾 ) ‘ 𝑊 ) )
76 9 74 75 syl2anc ⊢ ( 𝜑 → ( ⊥ ‘ 𝐵 ) ∈ ran ( ( DIsoH ‘ 𝐾 ) ‘ 𝑊 ) )
77 1 16 3 4 2 17 9 72 76 dochdmm1 ⊢ ( 𝜑 → ( ⊥ ‘ ( ( ( 𝑁 ‘ { 𝑋 } ) ⊕ ( 𝑁 ‘ { 𝑌 } ) ) ∩ ( ⊥ ‘ 𝐵 ) ) ) = ( ( ⊥ ‘ ( ( 𝑁 ‘ { 𝑋 } ) ⊕ ( 𝑁 ‘ { 𝑌 } ) ) ) ( ( joinH ‘ 𝐾 ) ‘ 𝑊 ) ( ⊥ ‘ ( ⊥ ‘ 𝐵 ) ) ) )
78 60 fveq2d ⊢ ( 𝜑 → ( ⊥ ‘ ( 𝑁 ‘ { 𝑋 , 𝑌 } ) ) = ( ⊥ ‘ ( ( 𝑁 ‘ { 𝑋 } ) ⊕ ( 𝑁 ‘ { 𝑌 } ) ) ) )
79 1 3 2 4 7 9 31 dochocsp ⊢ ( 𝜑 → ( ⊥ ‘ ( 𝑁 ‘ { 𝑋 , 𝑌 } ) ) = ( ⊥ ‘ { 𝑋 , 𝑌 } ) )
80 78 79 eqtr3d ⊢ ( 𝜑 → ( ⊥ ‘ ( ( 𝑁 ‘ { 𝑋 } ) ⊕ ( 𝑁 ‘ { 𝑌 } ) ) ) = ( ⊥ ‘ { 𝑋 , 𝑌 } ) )
81 1 3 16 8 dih1dimat ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐵 ∈ 𝐴 ) → 𝐵 ∈ ran ( ( DIsoH ‘ 𝐾 ) ‘ 𝑊 ) )
82 9 73 81 syl2anc ⊢ ( 𝜑 → 𝐵 ∈ ran ( ( DIsoH ‘ 𝐾 ) ‘ 𝑊 ) )
83 1 16 2 dochoc ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐵 ∈ ran ( ( DIsoH ‘ 𝐾 ) ‘ 𝑊 ) ) → ( ⊥ ‘ ( ⊥ ‘ 𝐵 ) ) = 𝐵 )
84 9 82 83 syl2anc ⊢ ( 𝜑 → ( ⊥ ‘ ( ⊥ ‘ 𝐵 ) ) = 𝐵 )
85 80 84 oveq12d ⊢ ( 𝜑 → ( ( ⊥ ‘ ( ( 𝑁 ‘ { 𝑋 } ) ⊕ ( 𝑁 ‘ { 𝑌 } ) ) ) ( ( joinH ‘ 𝐾 ) ‘ 𝑊 ) ( ⊥ ‘ ( ⊥ ‘ 𝐵 ) ) ) = ( ( ⊥ ‘ { 𝑋 , 𝑌 } ) ( ( joinH ‘ 𝐾 ) ‘ 𝑊 ) 𝐵 ) )
86 1 16 3 4 2 dochcl ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ { 𝑋 , 𝑌 } ⊆ 𝑉 ) → ( ⊥ ‘ { 𝑋 , 𝑌 } ) ∈ ran ( ( DIsoH ‘ 𝐾 ) ‘ 𝑊 ) )
87 9 31 86 syl2anc ⊢ ( 𝜑 → ( ⊥ ‘ { 𝑋 , 𝑌 } ) ∈ ran ( ( DIsoH ‘ 𝐾 ) ‘ 𝑊 ) )
88 1 16 17 3 14 8 9 87 73 dihjat2 ⊢ ( 𝜑 → ( ( ⊥ ‘ { 𝑋 , 𝑌 } ) ( ( joinH ‘ 𝐾 ) ‘ 𝑊 ) 𝐵 ) = ( ( ⊥ ‘ { 𝑋 , 𝑌 } ) ⊕ 𝐵 ) )
89 77 85 88 3eqtrd ⊢ ( 𝜑 → ( ⊥ ‘ ( ( ( 𝑁 ‘ { 𝑋 } ) ⊕ ( 𝑁 ‘ { 𝑌 } ) ) ∩ ( ⊥ ‘ 𝐵 ) ) ) = ( ( ⊥ ‘ { 𝑋 , 𝑌 } ) ⊕ 𝐵 ) )
90 1 3 2 4 7 9 24 dochocsp ⊢ ( 𝜑 → ( ⊥ ‘ ( 𝑁 ‘ { ( 𝑋 + 𝑌 ) } ) ) = ( ⊥ ‘ { ( 𝑋 + 𝑌 ) } ) )
91 71 89 90 3eqtr3d ⊢ ( 𝜑 → ( ( ⊥ ‘ { 𝑋 , 𝑌 } ) ⊕ 𝐵 ) = ( ⊥ ‘ { ( 𝑋 + 𝑌 ) } ) )