Metamath Proof Explorer

Theorem dochnoncon

Description: Law of noncontradiction. The intersection of a subspace and its orthocomplement is the zero subspace. (Contributed by NM, 16-Apr-2014)

Ref Expression
Hypotheses dochnoncon.h ⊢ 𝐻 = ( LHyp ‘ 𝐾 )
dochnoncon.u ⊢ 𝑈 = ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 )
dochnoncon.s ⊢ 𝑆 = ( LSubSp ‘ 𝑈 )
dochnoncon.z ⊢ 0 = ( 0g ‘ 𝑈 )
dochnoncon.o ⊢ ⊥ = ( ( ocH ‘ 𝐾 ) ‘ 𝑊 )
Assertion dochnoncon ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑋 ∈ 𝑆 ) → ( 𝑋 ∩ ( ⊥ ‘ 𝑋 ) ) = { 0 } )

Proof

Step Hyp Ref Expression
1 dochnoncon.h ⊢ 𝐻 = ( LHyp ‘ 𝐾 )
2 dochnoncon.u ⊢ 𝑈 = ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 )
3 dochnoncon.s ⊢ 𝑆 = ( LSubSp ‘ 𝑈 )
4 dochnoncon.z ⊢ 0 = ( 0g ‘ 𝑈 )
5 dochnoncon.o ⊢ ⊥ = ( ( ocH ‘ 𝐾 ) ‘ 𝑊 )
6 eqid ⊢ ( Base ‘ 𝑈 ) = ( Base ‘ 𝑈 )
7 6 3 lssss ⊢ ( 𝑋 ∈ 𝑆 → 𝑋 ⊆ ( Base ‘ 𝑈 ) )
8 1 2 6 5 dochocss ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑋 ⊆ ( Base ‘ 𝑈 ) ) → 𝑋 ⊆ ( ⊥ ‘ ( ⊥ ‘ 𝑋 ) ) )
9 7 8 sylan2 ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑋 ∈ 𝑆 ) → 𝑋 ⊆ ( ⊥ ‘ ( ⊥ ‘ 𝑋 ) ) )
10 9 ssrind ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑋 ∈ 𝑆 ) → ( 𝑋 ∩ ( ⊥ ‘ 𝑋 ) ) ⊆ ( ( ⊥ ‘ ( ⊥ ‘ 𝑋 ) ) ∩ ( ⊥ ‘ 𝑋 ) ) )
11 simpl ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑋 ∈ 𝑆 ) → ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) )
12 eqid ⊢ ( Base ‘ 𝐾 ) = ( Base ‘ 𝐾 )
13 eqid ⊢ ( ( DIsoH ‘ 𝐾 ) ‘ 𝑊 ) = ( ( DIsoH ‘ 𝐾 ) ‘ 𝑊 )
14 eqid ⊢ ( LSubSp ‘ 𝑈 ) = ( LSubSp ‘ 𝑈 )
15 12 1 13 2 14 dihf11 ⊢ ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) → ( ( DIsoH ‘ 𝐾 ) ‘ 𝑊 ) : ( Base ‘ 𝐾 ) –1-1→ ( LSubSp ‘ 𝑈 ) )
16 15 adantr ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑋 ∈ 𝑆 ) → ( ( DIsoH ‘ 𝐾 ) ‘ 𝑊 ) : ( Base ‘ 𝐾 ) –1-1→ ( LSubSp ‘ 𝑈 ) )
17 f1f1orn ⊢ ( ( ( DIsoH ‘ 𝐾 ) ‘ 𝑊 ) : ( Base ‘ 𝐾 ) –1-1→ ( LSubSp ‘ 𝑈 ) → ( ( DIsoH ‘ 𝐾 ) ‘ 𝑊 ) : ( Base ‘ 𝐾 ) –1-1-onto→ ran ( ( DIsoH ‘ 𝐾 ) ‘ 𝑊 ) )
18 16 17 syl ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑋 ∈ 𝑆 ) → ( ( DIsoH ‘ 𝐾 ) ‘ 𝑊 ) : ( Base ‘ 𝐾 ) –1-1-onto→ ran ( ( DIsoH ‘ 𝐾 ) ‘ 𝑊 ) )
19 1 13 2 6 5 dochcl ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑋 ⊆ ( Base ‘ 𝑈 ) ) → ( ⊥ ‘ 𝑋 ) ∈ ran ( ( DIsoH ‘ 𝐾 ) ‘ 𝑊 ) )
20 7 19 sylan2 ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑋 ∈ 𝑆 ) → ( ⊥ ‘ 𝑋 ) ∈ ran ( ( DIsoH ‘ 𝐾 ) ‘ 𝑊 ) )
21 1 2 13 14 dihrnlss ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( ⊥ ‘ 𝑋 ) ∈ ran ( ( DIsoH ‘ 𝐾 ) ‘ 𝑊 ) ) → ( ⊥ ‘ 𝑋 ) ∈ ( LSubSp ‘ 𝑈 ) )
22 20 21 syldan ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑋 ∈ 𝑆 ) → ( ⊥ ‘ 𝑋 ) ∈ ( LSubSp ‘ 𝑈 ) )
23 6 14 lssss ⊢ ( ( ⊥ ‘ 𝑋 ) ∈ ( LSubSp ‘ 𝑈 ) → ( ⊥ ‘ 𝑋 ) ⊆ ( Base ‘ 𝑈 ) )
24 22 23 syl ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑋 ∈ 𝑆 ) → ( ⊥ ‘ 𝑋 ) ⊆ ( Base ‘ 𝑈 ) )
25 1 13 2 6 5 dochcl ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( ⊥ ‘ 𝑋 ) ⊆ ( Base ‘ 𝑈 ) ) → ( ⊥ ‘ ( ⊥ ‘ 𝑋 ) ) ∈ ran ( ( DIsoH ‘ 𝐾 ) ‘ 𝑊 ) )
26 24 25 syldan ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑋 ∈ 𝑆 ) → ( ⊥ ‘ ( ⊥ ‘ 𝑋 ) ) ∈ ran ( ( DIsoH ‘ 𝐾 ) ‘ 𝑊 ) )
27 f1ocnvdm ⊢ ( ( ( ( DIsoH ‘ 𝐾 ) ‘ 𝑊 ) : ( Base ‘ 𝐾 ) –1-1-onto→ ran ( ( DIsoH ‘ 𝐾 ) ‘ 𝑊 ) ∧ ( ⊥ ‘ ( ⊥ ‘ 𝑋 ) ) ∈ ran ( ( DIsoH ‘ 𝐾 ) ‘ 𝑊 ) ) → ( ◡ ( ( DIsoH ‘ 𝐾 ) ‘ 𝑊 ) ‘ ( ⊥ ‘ ( ⊥ ‘ 𝑋 ) ) ) ∈ ( Base ‘ 𝐾 ) )
28 18 26 27 syl2anc ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑋 ∈ 𝑆 ) → ( ◡ ( ( DIsoH ‘ 𝐾 ) ‘ 𝑊 ) ‘ ( ⊥ ‘ ( ⊥ ‘ 𝑋 ) ) ) ∈ ( Base ‘ 𝐾 ) )
29 hlop ⊢ ( 𝐾 ∈ HL → 𝐾 ∈ OP )
30 29 ad2antrr ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑋 ∈ 𝑆 ) → 𝐾 ∈ OP )
31 eqid ⊢ ( oc ‘ 𝐾 ) = ( oc ‘ 𝐾 )
32 12 31 opoccl ⊢ ( ( 𝐾 ∈ OP ∧ ( ◡ ( ( DIsoH ‘ 𝐾 ) ‘ 𝑊 ) ‘ ( ⊥ ‘ ( ⊥ ‘ 𝑋 ) ) ) ∈ ( Base ‘ 𝐾 ) ) → ( ( oc ‘ 𝐾 ) ‘ ( ◡ ( ( DIsoH ‘ 𝐾 ) ‘ 𝑊 ) ‘ ( ⊥ ‘ ( ⊥ ‘ 𝑋 ) ) ) ) ∈ ( Base ‘ 𝐾 ) )
33 30 28 32 syl2anc ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑋 ∈ 𝑆 ) → ( ( oc ‘ 𝐾 ) ‘ ( ◡ ( ( DIsoH ‘ 𝐾 ) ‘ 𝑊 ) ‘ ( ⊥ ‘ ( ⊥ ‘ 𝑋 ) ) ) ) ∈ ( Base ‘ 𝐾 ) )
34 eqid ⊢ ( meet ‘ 𝐾 ) = ( meet ‘ 𝐾 )
35 12 34 1 13 dihmeet ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( ◡ ( ( DIsoH ‘ 𝐾 ) ‘ 𝑊 ) ‘ ( ⊥ ‘ ( ⊥ ‘ 𝑋 ) ) ) ∈ ( Base ‘ 𝐾 ) ∧ ( ( oc ‘ 𝐾 ) ‘ ( ◡ ( ( DIsoH ‘ 𝐾 ) ‘ 𝑊 ) ‘ ( ⊥ ‘ ( ⊥ ‘ 𝑋 ) ) ) ) ∈ ( Base ‘ 𝐾 ) ) → ( ( ( DIsoH ‘ 𝐾 ) ‘ 𝑊 ) ‘ ( ( ◡ ( ( DIsoH ‘ 𝐾 ) ‘ 𝑊 ) ‘ ( ⊥ ‘ ( ⊥ ‘ 𝑋 ) ) ) ( meet ‘ 𝐾 ) ( ( oc ‘ 𝐾 ) ‘ ( ◡ ( ( DIsoH ‘ 𝐾 ) ‘ 𝑊 ) ‘ ( ⊥ ‘ ( ⊥ ‘ 𝑋 ) ) ) ) ) ) = ( ( ( ( DIsoH ‘ 𝐾 ) ‘ 𝑊 ) ‘ ( ◡ ( ( DIsoH ‘ 𝐾 ) ‘ 𝑊 ) ‘ ( ⊥ ‘ ( ⊥ ‘ 𝑋 ) ) ) ) ∩ ( ( ( DIsoH ‘ 𝐾 ) ‘ 𝑊 ) ‘ ( ( oc ‘ 𝐾 ) ‘ ( ◡ ( ( DIsoH ‘ 𝐾 ) ‘ 𝑊 ) ‘ ( ⊥ ‘ ( ⊥ ‘ 𝑋 ) ) ) ) ) ) )
36 11 28 33 35 syl3anc ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑋 ∈ 𝑆 ) → ( ( ( DIsoH ‘ 𝐾 ) ‘ 𝑊 ) ‘ ( ( ◡ ( ( DIsoH ‘ 𝐾 ) ‘ 𝑊 ) ‘ ( ⊥ ‘ ( ⊥ ‘ 𝑋 ) ) ) ( meet ‘ 𝐾 ) ( ( oc ‘ 𝐾 ) ‘ ( ◡ ( ( DIsoH ‘ 𝐾 ) ‘ 𝑊 ) ‘ ( ⊥ ‘ ( ⊥ ‘ 𝑋 ) ) ) ) ) ) = ( ( ( ( DIsoH ‘ 𝐾 ) ‘ 𝑊 ) ‘ ( ◡ ( ( DIsoH ‘ 𝐾 ) ‘ 𝑊 ) ‘ ( ⊥ ‘ ( ⊥ ‘ 𝑋 ) ) ) ) ∩ ( ( ( DIsoH ‘ 𝐾 ) ‘ 𝑊 ) ‘ ( ( oc ‘ 𝐾 ) ‘ ( ◡ ( ( DIsoH ‘ 𝐾 ) ‘ 𝑊 ) ‘ ( ⊥ ‘ ( ⊥ ‘ 𝑋 ) ) ) ) ) ) )
37 eqid ⊢ ( 0. ‘ 𝐾 ) = ( 0. ‘ 𝐾 )
38 12 31 34 37 opnoncon ⊢ ( ( 𝐾 ∈ OP ∧ ( ◡ ( ( DIsoH ‘ 𝐾 ) ‘ 𝑊 ) ‘ ( ⊥ ‘ ( ⊥ ‘ 𝑋 ) ) ) ∈ ( Base ‘ 𝐾 ) ) → ( ( ◡ ( ( DIsoH ‘ 𝐾 ) ‘ 𝑊 ) ‘ ( ⊥ ‘ ( ⊥ ‘ 𝑋 ) ) ) ( meet ‘ 𝐾 ) ( ( oc ‘ 𝐾 ) ‘ ( ◡ ( ( DIsoH ‘ 𝐾 ) ‘ 𝑊 ) ‘ ( ⊥ ‘ ( ⊥ ‘ 𝑋 ) ) ) ) ) = ( 0. ‘ 𝐾 ) )
39 30 28 38 syl2anc ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑋 ∈ 𝑆 ) → ( ( ◡ ( ( DIsoH ‘ 𝐾 ) ‘ 𝑊 ) ‘ ( ⊥ ‘ ( ⊥ ‘ 𝑋 ) ) ) ( meet ‘ 𝐾 ) ( ( oc ‘ 𝐾 ) ‘ ( ◡ ( ( DIsoH ‘ 𝐾 ) ‘ 𝑊 ) ‘ ( ⊥ ‘ ( ⊥ ‘ 𝑋 ) ) ) ) ) = ( 0. ‘ 𝐾 ) )
40 39 fveq2d ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑋 ∈ 𝑆 ) → ( ( ( DIsoH ‘ 𝐾 ) ‘ 𝑊 ) ‘ ( ( ◡ ( ( DIsoH ‘ 𝐾 ) ‘ 𝑊 ) ‘ ( ⊥ ‘ ( ⊥ ‘ 𝑋 ) ) ) ( meet ‘ 𝐾 ) ( ( oc ‘ 𝐾 ) ‘ ( ◡ ( ( DIsoH ‘ 𝐾 ) ‘ 𝑊 ) ‘ ( ⊥ ‘ ( ⊥ ‘ 𝑋 ) ) ) ) ) ) = ( ( ( DIsoH ‘ 𝐾 ) ‘ 𝑊 ) ‘ ( 0. ‘ 𝐾 ) ) )
41 36 40 eqtr3d ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑋 ∈ 𝑆 ) → ( ( ( ( DIsoH ‘ 𝐾 ) ‘ 𝑊 ) ‘ ( ◡ ( ( DIsoH ‘ 𝐾 ) ‘ 𝑊 ) ‘ ( ⊥ ‘ ( ⊥ ‘ 𝑋 ) ) ) ) ∩ ( ( ( DIsoH ‘ 𝐾 ) ‘ 𝑊 ) ‘ ( ( oc ‘ 𝐾 ) ‘ ( ◡ ( ( DIsoH ‘ 𝐾 ) ‘ 𝑊 ) ‘ ( ⊥ ‘ ( ⊥ ‘ 𝑋 ) ) ) ) ) ) = ( ( ( DIsoH ‘ 𝐾 ) ‘ 𝑊 ) ‘ ( 0. ‘ 𝐾 ) ) )
42 1 13 dihcnvid2 ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( ⊥ ‘ ( ⊥ ‘ 𝑋 ) ) ∈ ran ( ( DIsoH ‘ 𝐾 ) ‘ 𝑊 ) ) → ( ( ( DIsoH ‘ 𝐾 ) ‘ 𝑊 ) ‘ ( ◡ ( ( DIsoH ‘ 𝐾 ) ‘ 𝑊 ) ‘ ( ⊥ ‘ ( ⊥ ‘ 𝑋 ) ) ) ) = ( ⊥ ‘ ( ⊥ ‘ 𝑋 ) ) )
43 26 42 syldan ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑋 ∈ 𝑆 ) → ( ( ( DIsoH ‘ 𝐾 ) ‘ 𝑊 ) ‘ ( ◡ ( ( DIsoH ‘ 𝐾 ) ‘ 𝑊 ) ‘ ( ⊥ ‘ ( ⊥ ‘ 𝑋 ) ) ) ) = ( ⊥ ‘ ( ⊥ ‘ 𝑋 ) ) )
44 31 1 13 5 dochvalr ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( ⊥ ‘ ( ⊥ ‘ 𝑋 ) ) ∈ ran ( ( DIsoH ‘ 𝐾 ) ‘ 𝑊 ) ) → ( ⊥ ‘ ( ⊥ ‘ ( ⊥ ‘ 𝑋 ) ) ) = ( ( ( DIsoH ‘ 𝐾 ) ‘ 𝑊 ) ‘ ( ( oc ‘ 𝐾 ) ‘ ( ◡ ( ( DIsoH ‘ 𝐾 ) ‘ 𝑊 ) ‘ ( ⊥ ‘ ( ⊥ ‘ 𝑋 ) ) ) ) ) )
45 26 44 syldan ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑋 ∈ 𝑆 ) → ( ⊥ ‘ ( ⊥ ‘ ( ⊥ ‘ 𝑋 ) ) ) = ( ( ( DIsoH ‘ 𝐾 ) ‘ 𝑊 ) ‘ ( ( oc ‘ 𝐾 ) ‘ ( ◡ ( ( DIsoH ‘ 𝐾 ) ‘ 𝑊 ) ‘ ( ⊥ ‘ ( ⊥ ‘ 𝑋 ) ) ) ) ) )
46 1 13 5 dochoc ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( ⊥ ‘ 𝑋 ) ∈ ran ( ( DIsoH ‘ 𝐾 ) ‘ 𝑊 ) ) → ( ⊥ ‘ ( ⊥ ‘ ( ⊥ ‘ 𝑋 ) ) ) = ( ⊥ ‘ 𝑋 ) )
47 20 46 syldan ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑋 ∈ 𝑆 ) → ( ⊥ ‘ ( ⊥ ‘ ( ⊥ ‘ 𝑋 ) ) ) = ( ⊥ ‘ 𝑋 ) )
48 45 47 eqtr3d ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑋 ∈ 𝑆 ) → ( ( ( DIsoH ‘ 𝐾 ) ‘ 𝑊 ) ‘ ( ( oc ‘ 𝐾 ) ‘ ( ◡ ( ( DIsoH ‘ 𝐾 ) ‘ 𝑊 ) ‘ ( ⊥ ‘ ( ⊥ ‘ 𝑋 ) ) ) ) ) = ( ⊥ ‘ 𝑋 ) )
49 43 48 ineq12d ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑋 ∈ 𝑆 ) → ( ( ( ( DIsoH ‘ 𝐾 ) ‘ 𝑊 ) ‘ ( ◡ ( ( DIsoH ‘ 𝐾 ) ‘ 𝑊 ) ‘ ( ⊥ ‘ ( ⊥ ‘ 𝑋 ) ) ) ) ∩ ( ( ( DIsoH ‘ 𝐾 ) ‘ 𝑊 ) ‘ ( ( oc ‘ 𝐾 ) ‘ ( ◡ ( ( DIsoH ‘ 𝐾 ) ‘ 𝑊 ) ‘ ( ⊥ ‘ ( ⊥ ‘ 𝑋 ) ) ) ) ) ) = ( ( ⊥ ‘ ( ⊥ ‘ 𝑋 ) ) ∩ ( ⊥ ‘ 𝑋 ) ) )
50 37 1 13 2 4 dih0 ⊢ ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) → ( ( ( DIsoH ‘ 𝐾 ) ‘ 𝑊 ) ‘ ( 0. ‘ 𝐾 ) ) = { 0 } )
51 50 adantr ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑋 ∈ 𝑆 ) → ( ( ( DIsoH ‘ 𝐾 ) ‘ 𝑊 ) ‘ ( 0. ‘ 𝐾 ) ) = { 0 } )
52 41 49 51 3eqtr3d ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑋 ∈ 𝑆 ) → ( ( ⊥ ‘ ( ⊥ ‘ 𝑋 ) ) ∩ ( ⊥ ‘ 𝑋 ) ) = { 0 } )
53 10 52 sseqtrd ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑋 ∈ 𝑆 ) → ( 𝑋 ∩ ( ⊥ ‘ 𝑋 ) ) ⊆ { 0 } )
54 1 2 11 dvhlmod ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑋 ∈ 𝑆 ) → 𝑈 ∈ LMod )
55 simpr ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑋 ∈ 𝑆 ) → 𝑋 ∈ 𝑆 )
56 1 2 13 3 dihrnlss ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( ⊥ ‘ 𝑋 ) ∈ ran ( ( DIsoH ‘ 𝐾 ) ‘ 𝑊 ) ) → ( ⊥ ‘ 𝑋 ) ∈ 𝑆 )
57 20 56 syldan ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑋 ∈ 𝑆 ) → ( ⊥ ‘ 𝑋 ) ∈ 𝑆 )
58 3 lssincl ⊢ ( ( 𝑈 ∈ LMod ∧ 𝑋 ∈ 𝑆 ∧ ( ⊥ ‘ 𝑋 ) ∈ 𝑆 ) → ( 𝑋 ∩ ( ⊥ ‘ 𝑋 ) ) ∈ 𝑆 )
59 54 55 57 58 syl3anc ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑋 ∈ 𝑆 ) → ( 𝑋 ∩ ( ⊥ ‘ 𝑋 ) ) ∈ 𝑆 )
60 4 3 lss0ss ⊢ ( ( 𝑈 ∈ LMod ∧ ( 𝑋 ∩ ( ⊥ ‘ 𝑋 ) ) ∈ 𝑆 ) → { 0 } ⊆ ( 𝑋 ∩ ( ⊥ ‘ 𝑋 ) ) )
61 54 59 60 syl2anc ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑋 ∈ 𝑆 ) → { 0 } ⊆ ( 𝑋 ∩ ( ⊥ ‘ 𝑋 ) ) )
62 53 61 eqssd ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑋 ∈ 𝑆 ) → ( 𝑋 ∩ ( ⊥ ‘ 𝑋 ) ) = { 0 } )