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
|
syl5eq |
⊢ ( 𝜑 → ( ⊥ ‘ 𝐵 ) = ( ( ⊥ ‘ ( 𝑁 ‘ { 𝑋 , 𝑌 } ) ) ⊕ ( 𝑁 ‘ { ( 𝑋 + 𝑌 ) } ) ) ) |
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 |
⊢ ( 𝜑 → ( ( ⊥ ‘ { 𝑋 , 𝑌 } ) ⊕ 𝐵 ) = ( ⊥ ‘ { ( 𝑋 + 𝑌 ) } ) ) |