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

Metamath Proof Explorer

Theorem dochsat

Description: The double orthocomplement of an atom is an atom. (Contributed by NM, 29-Oct-2014)

Ref Expression
Hypotheses dochsat.h ⊢ 𝐻 = ( LHyp ‘ 𝐾 )
dochsat.o ⊢ ⊥ = ( ( ocH ‘ 𝐾 ) ‘ 𝑊 )
dochsat.u ⊢ 𝑈 = ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 )
dochsat.s ⊢ 𝑆 = ( LSubSp ‘ 𝑈 )
dochsat.a ⊢ 𝐴 = ( LSAtoms ‘ 𝑈 )
dochsat.k ⊢ ( 𝜑 → ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) )
dochsat.q ⊢ ( 𝜑 → 𝑄 ∈ 𝑆 )
Assertion dochsat ( 𝜑 → ( ( ⊥ ‘ ( ⊥ ‘ 𝑄 ) ) ∈ 𝐴 ↔ 𝑄 ∈ 𝐴 ) )

Proof

Step Hyp Ref Expression
1 dochsat.h ⊢ 𝐻 = ( LHyp ‘ 𝐾 )
2 dochsat.o ⊢ ⊥ = ( ( ocH ‘ 𝐾 ) ‘ 𝑊 )
3 dochsat.u ⊢ 𝑈 = ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 )
4 dochsat.s ⊢ 𝑆 = ( LSubSp ‘ 𝑈 )
5 dochsat.a ⊢ 𝐴 = ( LSAtoms ‘ 𝑈 )
6 dochsat.k ⊢ ( 𝜑 → ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) )
7 dochsat.q ⊢ ( 𝜑 → 𝑄 ∈ 𝑆 )
8 1 3 6 dvhlmod ⊢ ( 𝜑 → 𝑈 ∈ LMod )
9 8 adantr ⊢ ( ( 𝜑 ∧ ( ⊥ ‘ ( ⊥ ‘ 𝑄 ) ) ∈ 𝐴 ) → 𝑈 ∈ LMod )
10 7 adantr ⊢ ( ( 𝜑 ∧ ( ⊥ ‘ ( ⊥ ‘ 𝑄 ) ) ∈ 𝐴 ) → 𝑄 ∈ 𝑆 )
11 eqid ⊢ ( 0g ‘ 𝑈 ) = ( 0g ‘ 𝑈 )
12 11 4 lss0ss ⊢ ( ( 𝑈 ∈ LMod ∧ 𝑄 ∈ 𝑆 ) → { ( 0g ‘ 𝑈 ) } ⊆ 𝑄 )
13 9 10 12 syl2anc ⊢ ( ( 𝜑 ∧ ( ⊥ ‘ ( ⊥ ‘ 𝑄 ) ) ∈ 𝐴 ) → { ( 0g ‘ 𝑈 ) } ⊆ 𝑄 )
14 simpr ⊢ ( ( 𝜑 ∧ ( ⊥ ‘ ( ⊥ ‘ 𝑄 ) ) ∈ 𝐴 ) → ( ⊥ ‘ ( ⊥ ‘ 𝑄 ) ) ∈ 𝐴 )
15 11 5 9 14 lsatn0 ⊢ ( ( 𝜑 ∧ ( ⊥ ‘ ( ⊥ ‘ 𝑄 ) ) ∈ 𝐴 ) → ( ⊥ ‘ ( ⊥ ‘ 𝑄 ) ) ≠ { ( 0g ‘ 𝑈 ) } )
16 simpr ⊢ ( ( ( 𝜑 ∧ ( ⊥ ‘ ( ⊥ ‘ 𝑄 ) ) ∈ 𝐴 ) ∧ 𝑄 = { ( 0g ‘ 𝑈 ) } ) → 𝑄 = { ( 0g ‘ 𝑈 ) } )
17 16 fveq2d ⊢ ( ( ( 𝜑 ∧ ( ⊥ ‘ ( ⊥ ‘ 𝑄 ) ) ∈ 𝐴 ) ∧ 𝑄 = { ( 0g ‘ 𝑈 ) } ) → ( ⊥ ‘ 𝑄 ) = ( ⊥ ‘ { ( 0g ‘ 𝑈 ) } ) )
18 17 fveq2d ⊢ ( ( ( 𝜑 ∧ ( ⊥ ‘ ( ⊥ ‘ 𝑄 ) ) ∈ 𝐴 ) ∧ 𝑄 = { ( 0g ‘ 𝑈 ) } ) → ( ⊥ ‘ ( ⊥ ‘ 𝑄 ) ) = ( ⊥ ‘ ( ⊥ ‘ { ( 0g ‘ 𝑈 ) } ) ) )
19 1 3 2 11 6 dochoc0 ⊢ ( 𝜑 → ( ⊥ ‘ ( ⊥ ‘ { ( 0g ‘ 𝑈 ) } ) ) = { ( 0g ‘ 𝑈 ) } )
20 19 adantr ⊢ ( ( 𝜑 ∧ ( ⊥ ‘ ( ⊥ ‘ 𝑄 ) ) ∈ 𝐴 ) → ( ⊥ ‘ ( ⊥ ‘ { ( 0g ‘ 𝑈 ) } ) ) = { ( 0g ‘ 𝑈 ) } )
21 20 adantr ⊢ ( ( ( 𝜑 ∧ ( ⊥ ‘ ( ⊥ ‘ 𝑄 ) ) ∈ 𝐴 ) ∧ 𝑄 = { ( 0g ‘ 𝑈 ) } ) → ( ⊥ ‘ ( ⊥ ‘ { ( 0g ‘ 𝑈 ) } ) ) = { ( 0g ‘ 𝑈 ) } )
22 18 21 eqtrd ⊢ ( ( ( 𝜑 ∧ ( ⊥ ‘ ( ⊥ ‘ 𝑄 ) ) ∈ 𝐴 ) ∧ 𝑄 = { ( 0g ‘ 𝑈 ) } ) → ( ⊥ ‘ ( ⊥ ‘ 𝑄 ) ) = { ( 0g ‘ 𝑈 ) } )
23 22 ex ⊢ ( ( 𝜑 ∧ ( ⊥ ‘ ( ⊥ ‘ 𝑄 ) ) ∈ 𝐴 ) → ( 𝑄 = { ( 0g ‘ 𝑈 ) } → ( ⊥ ‘ ( ⊥ ‘ 𝑄 ) ) = { ( 0g ‘ 𝑈 ) } ) )
24 23 necon3d ⊢ ( ( 𝜑 ∧ ( ⊥ ‘ ( ⊥ ‘ 𝑄 ) ) ∈ 𝐴 ) → ( ( ⊥ ‘ ( ⊥ ‘ 𝑄 ) ) ≠ { ( 0g ‘ 𝑈 ) } → 𝑄 ≠ { ( 0g ‘ 𝑈 ) } ) )
25 15 24 mpd ⊢ ( ( 𝜑 ∧ ( ⊥ ‘ ( ⊥ ‘ 𝑄 ) ) ∈ 𝐴 ) → 𝑄 ≠ { ( 0g ‘ 𝑈 ) } )
26 25 necomd ⊢ ( ( 𝜑 ∧ ( ⊥ ‘ ( ⊥ ‘ 𝑄 ) ) ∈ 𝐴 ) → { ( 0g ‘ 𝑈 ) } ≠ 𝑄 )
27 df-pss ⊢ ( { ( 0g ‘ 𝑈 ) } ⊊ 𝑄 ↔ ( { ( 0g ‘ 𝑈 ) } ⊆ 𝑄 ∧ { ( 0g ‘ 𝑈 ) } ≠ 𝑄 ) )
28 13 26 27 sylanbrc ⊢ ( ( 𝜑 ∧ ( ⊥ ‘ ( ⊥ ‘ 𝑄 ) ) ∈ 𝐴 ) → { ( 0g ‘ 𝑈 ) } ⊊ 𝑄 )
29 6 adantr ⊢ ( ( 𝜑 ∧ ( ⊥ ‘ ( ⊥ ‘ 𝑄 ) ) ∈ 𝐴 ) → ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) )
30 eqid ⊢ ( Base ‘ 𝑈 ) = ( Base ‘ 𝑈 )
31 30 4 lssss ⊢ ( 𝑄 ∈ 𝑆 → 𝑄 ⊆ ( Base ‘ 𝑈 ) )
32 7 31 syl ⊢ ( 𝜑 → 𝑄 ⊆ ( Base ‘ 𝑈 ) )
33 32 adantr ⊢ ( ( 𝜑 ∧ ( ⊥ ‘ ( ⊥ ‘ 𝑄 ) ) ∈ 𝐴 ) → 𝑄 ⊆ ( Base ‘ 𝑈 ) )
34 1 3 30 2 dochocss ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑄 ⊆ ( Base ‘ 𝑈 ) ) → 𝑄 ⊆ ( ⊥ ‘ ( ⊥ ‘ 𝑄 ) ) )
35 29 33 34 syl2anc ⊢ ( ( 𝜑 ∧ ( ⊥ ‘ ( ⊥ ‘ 𝑄 ) ) ∈ 𝐴 ) → 𝑄 ⊆ ( ⊥ ‘ ( ⊥ ‘ 𝑄 ) ) )
36 4 5 9 14 lsatlssel ⊢ ( ( 𝜑 ∧ ( ⊥ ‘ ( ⊥ ‘ 𝑄 ) ) ∈ 𝐴 ) → ( ⊥ ‘ ( ⊥ ‘ 𝑄 ) ) ∈ 𝑆 )
37 4 lsssubg ⊢ ( ( 𝑈 ∈ LMod ∧ ( ⊥ ‘ ( ⊥ ‘ 𝑄 ) ) ∈ 𝑆 ) → ( ⊥ ‘ ( ⊥ ‘ 𝑄 ) ) ∈ ( SubGrp ‘ 𝑈 ) )
38 9 36 37 syl2anc ⊢ ( ( 𝜑 ∧ ( ⊥ ‘ ( ⊥ ‘ 𝑄 ) ) ∈ 𝐴 ) → ( ⊥ ‘ ( ⊥ ‘ 𝑄 ) ) ∈ ( SubGrp ‘ 𝑈 ) )
39 eqid ⊢ ( LSSum ‘ 𝑈 ) = ( LSSum ‘ 𝑈 )
40 11 39 lsm02 ⊢ ( ( ⊥ ‘ ( ⊥ ‘ 𝑄 ) ) ∈ ( SubGrp ‘ 𝑈 ) → ( { ( 0g ‘ 𝑈 ) } ( LSSum ‘ 𝑈 ) ( ⊥ ‘ ( ⊥ ‘ 𝑄 ) ) ) = ( ⊥ ‘ ( ⊥ ‘ 𝑄 ) ) )
41 38 40 syl ⊢ ( ( 𝜑 ∧ ( ⊥ ‘ ( ⊥ ‘ 𝑄 ) ) ∈ 𝐴 ) → ( { ( 0g ‘ 𝑈 ) } ( LSSum ‘ 𝑈 ) ( ⊥ ‘ ( ⊥ ‘ 𝑄 ) ) ) = ( ⊥ ‘ ( ⊥ ‘ 𝑄 ) ) )
42 35 41 sseqtrrd ⊢ ( ( 𝜑 ∧ ( ⊥ ‘ ( ⊥ ‘ 𝑄 ) ) ∈ 𝐴 ) → 𝑄 ⊆ ( { ( 0g ‘ 𝑈 ) } ( LSSum ‘ 𝑈 ) ( ⊥ ‘ ( ⊥ ‘ 𝑄 ) ) ) )
43 1 3 6 dvhlvec ⊢ ( 𝜑 → 𝑈 ∈ LVec )
44 43 adantr ⊢ ( ( 𝜑 ∧ ( ⊥ ‘ ( ⊥ ‘ 𝑄 ) ) ∈ 𝐴 ) → 𝑈 ∈ LVec )
45 11 4 lsssn0 ⊢ ( 𝑈 ∈ LMod → { ( 0g ‘ 𝑈 ) } ∈ 𝑆 )
46 9 45 syl ⊢ ( ( 𝜑 ∧ ( ⊥ ‘ ( ⊥ ‘ 𝑄 ) ) ∈ 𝐴 ) → { ( 0g ‘ 𝑈 ) } ∈ 𝑆 )
47 4 39 5 44 46 10 14 lsmsatcv ⊢ ( ( ( 𝜑 ∧ ( ⊥ ‘ ( ⊥ ‘ 𝑄 ) ) ∈ 𝐴 ) ∧ { ( 0g ‘ 𝑈 ) } ⊊ 𝑄 ∧ 𝑄 ⊆ ( { ( 0g ‘ 𝑈 ) } ( LSSum ‘ 𝑈 ) ( ⊥ ‘ ( ⊥ ‘ 𝑄 ) ) ) ) → 𝑄 = ( { ( 0g ‘ 𝑈 ) } ( LSSum ‘ 𝑈 ) ( ⊥ ‘ ( ⊥ ‘ 𝑄 ) ) ) )
48 28 42 47 mpd3an23 ⊢ ( ( 𝜑 ∧ ( ⊥ ‘ ( ⊥ ‘ 𝑄 ) ) ∈ 𝐴 ) → 𝑄 = ( { ( 0g ‘ 𝑈 ) } ( LSSum ‘ 𝑈 ) ( ⊥ ‘ ( ⊥ ‘ 𝑄 ) ) ) )
49 48 41 eqtr2d ⊢ ( ( 𝜑 ∧ ( ⊥ ‘ ( ⊥ ‘ 𝑄 ) ) ∈ 𝐴 ) → ( ⊥ ‘ ( ⊥ ‘ 𝑄 ) ) = 𝑄 )
50 49 14 eqeltrrd ⊢ ( ( 𝜑 ∧ ( ⊥ ‘ ( ⊥ ‘ 𝑄 ) ) ∈ 𝐴 ) → 𝑄 ∈ 𝐴 )
51 6 adantr ⊢ ( ( 𝜑 ∧ 𝑄 ∈ 𝐴 ) → ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) )
52 eqid ⊢ ( ( DIsoH ‘ 𝐾 ) ‘ 𝑊 ) = ( ( DIsoH ‘ 𝐾 ) ‘ 𝑊 )
53 1 3 52 5 dih1dimat ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑄 ∈ 𝐴 ) → 𝑄 ∈ ran ( ( DIsoH ‘ 𝐾 ) ‘ 𝑊 ) )
54 6 53 sylan ⊢ ( ( 𝜑 ∧ 𝑄 ∈ 𝐴 ) → 𝑄 ∈ ran ( ( DIsoH ‘ 𝐾 ) ‘ 𝑊 ) )
55 1 52 2 dochoc ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑄 ∈ ran ( ( DIsoH ‘ 𝐾 ) ‘ 𝑊 ) ) → ( ⊥ ‘ ( ⊥ ‘ 𝑄 ) ) = 𝑄 )
56 51 54 55 syl2anc ⊢ ( ( 𝜑 ∧ 𝑄 ∈ 𝐴 ) → ( ⊥ ‘ ( ⊥ ‘ 𝑄 ) ) = 𝑄 )
57 simpr ⊢ ( ( 𝜑 ∧ 𝑄 ∈ 𝐴 ) → 𝑄 ∈ 𝐴 )
58 56 57 eqeltrd ⊢ ( ( 𝜑 ∧ 𝑄 ∈ 𝐴 ) → ( ⊥ ‘ ( ⊥ ‘ 𝑄 ) ) ∈ 𝐴 )
59 50 58 impbida ⊢ ( 𝜑 → ( ( ⊥ ‘ ( ⊥ ‘ 𝑄 ) ) ∈ 𝐴 ↔ 𝑄 ∈ 𝐴 ) )