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	⊢ ( 𝜑 → ( ( ⊥ ‘ ( ⊥ ‘ 𝑄 ) ) ∈ 𝐴 ↔ 𝑄 ∈ 𝐴 ) )