Theorem dochexmid

Description: Excluded middle law for closed subspaces, which is equivalent to (and derived from) the orthomodular law dihoml4 . Lemma 3.3(2) in Holland95 p. 215. In our proof, we use the variables X , M , p , q , r in place of Hollands' l, m, P, Q, L respectively. ( pexmidALTN analog.) (Contributed by NM, 15-Jan-2015)

	Ref	Expression
Hypotheses	dochexmid.h	⊢ 𝐻 = ( LHyp ‘ 𝐾 )
	dochexmid.o	⊢ ⊥ = ( ( ocH ‘ 𝐾 ) ‘ 𝑊 )
	dochexmid.u	⊢ 𝑈 = ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 )
	dochexmid.v	⊢ 𝑉 = ( Base ‘ 𝑈 )
	dochexmid.s	⊢ 𝑆 = ( LSubSp ‘ 𝑈 )
	dochexmid.p	⊢ ⊕ = ( LSSum ‘ 𝑈 )
	dochexmid.k	⊢ ( 𝜑 → ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) )
	dochexmid.x	⊢ ( 𝜑 → 𝑋 ∈ 𝑆 )
	dochexmid.c	⊢ ( 𝜑 → ( ⊥ ‘ ( ⊥ ‘ 𝑋 ) ) = 𝑋 )
Assertion	dochexmid	⊢ ( 𝜑 → ( 𝑋 ⊕ ( ⊥ ‘ 𝑋 ) ) = 𝑉 )

Proof

Step	Hyp	Ref	Expression
1		dochexmid.h	⊢ 𝐻 = ( LHyp ‘ 𝐾 )
2		dochexmid.o	⊢ ⊥ = ( ( ocH ‘ 𝐾 ) ‘ 𝑊 )
3		dochexmid.u	⊢ 𝑈 = ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 )
4		dochexmid.v	⊢ 𝑉 = ( Base ‘ 𝑈 )
5		dochexmid.s	⊢ 𝑆 = ( LSubSp ‘ 𝑈 )
6		dochexmid.p	⊢ ⊕ = ( LSSum ‘ 𝑈 )
7		dochexmid.k	⊢ ( 𝜑 → ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) )
8		dochexmid.x	⊢ ( 𝜑 → 𝑋 ∈ 𝑆 )
9		dochexmid.c	⊢ ( 𝜑 → ( ⊥ ‘ ( ⊥ ‘ 𝑋 ) ) = 𝑋 )
10		id	⊢ ( 𝑋 = { ( 0g ‘ 𝑈 ) } → 𝑋 = { ( 0g ‘ 𝑈 ) } )
11		fveq2	⊢ ( 𝑋 = { ( 0g ‘ 𝑈 ) } → ( ⊥ ‘ 𝑋 ) = ( ⊥ ‘ { ( 0g ‘ 𝑈 ) } ) )
12	10 11	oveq12d	⊢ ( 𝑋 = { ( 0g ‘ 𝑈 ) } → ( 𝑋 ⊕ ( ⊥ ‘ 𝑋 ) ) = ( { ( 0g ‘ 𝑈 ) } ⊕ ( ⊥ ‘ { ( 0g ‘ 𝑈 ) } ) ) )
13	1 3 7	dvhlmod	⊢ ( 𝜑 → 𝑈 ∈ LMod )
14		eqid	⊢ ( 0g ‘ 𝑈 ) = ( 0g ‘ 𝑈 )
15	4 14	lmod0vcl	⊢ ( 𝑈 ∈ LMod → ( 0g ‘ 𝑈 ) ∈ 𝑉 )
16	13 15	syl	⊢ ( 𝜑 → ( 0g ‘ 𝑈 ) ∈ 𝑉 )
17	16	snssd	⊢ ( 𝜑 → { ( 0g ‘ 𝑈 ) } ⊆ 𝑉 )
18	1 3 4 5 2	dochlss	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ { ( 0g ‘ 𝑈 ) } ⊆ 𝑉 ) → ( ⊥ ‘ { ( 0g ‘ 𝑈 ) } ) ∈ 𝑆 )
19	7 17 18	syl2anc	⊢ ( 𝜑 → ( ⊥ ‘ { ( 0g ‘ 𝑈 ) } ) ∈ 𝑆 )
20	5	lsssubg	⊢ ( ( 𝑈 ∈ LMod ∧ ( ⊥ ‘ { ( 0g ‘ 𝑈 ) } ) ∈ 𝑆 ) → ( ⊥ ‘ { ( 0g ‘ 𝑈 ) } ) ∈ ( SubGrp ‘ 𝑈 ) )
21	13 19 20	syl2anc	⊢ ( 𝜑 → ( ⊥ ‘ { ( 0g ‘ 𝑈 ) } ) ∈ ( SubGrp ‘ 𝑈 ) )
22	14 6	lsm02	⊢ ( ( ⊥ ‘ { ( 0g ‘ 𝑈 ) } ) ∈ ( SubGrp ‘ 𝑈 ) → ( { ( 0g ‘ 𝑈 ) } ⊕ ( ⊥ ‘ { ( 0g ‘ 𝑈 ) } ) ) = ( ⊥ ‘ { ( 0g ‘ 𝑈 ) } ) )
23	21 22	syl	⊢ ( 𝜑 → ( { ( 0g ‘ 𝑈 ) } ⊕ ( ⊥ ‘ { ( 0g ‘ 𝑈 ) } ) ) = ( ⊥ ‘ { ( 0g ‘ 𝑈 ) } ) )
24	1 3 2 4 14	doch0	⊢ ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) → ( ⊥ ‘ { ( 0g ‘ 𝑈 ) } ) = 𝑉 )
25	7 24	syl	⊢ ( 𝜑 → ( ⊥ ‘ { ( 0g ‘ 𝑈 ) } ) = 𝑉 )
26	23 25	eqtrd	⊢ ( 𝜑 → ( { ( 0g ‘ 𝑈 ) } ⊕ ( ⊥ ‘ { ( 0g ‘ 𝑈 ) } ) ) = 𝑉 )
27	12 26	sylan9eqr	⊢ ( ( 𝜑 ∧ 𝑋 = { ( 0g ‘ 𝑈 ) } ) → ( 𝑋 ⊕ ( ⊥ ‘ 𝑋 ) ) = 𝑉 )
28		eqid	⊢ ( LSpan ‘ 𝑈 ) = ( LSpan ‘ 𝑈 )
29		eqid	⊢ ( LSAtoms ‘ 𝑈 ) = ( LSAtoms ‘ 𝑈 )
30	7	adantr	⊢ ( ( 𝜑 ∧ 𝑋 ≠ { ( 0g ‘ 𝑈 ) } ) → ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) )
31	8	adantr	⊢ ( ( 𝜑 ∧ 𝑋 ≠ { ( 0g ‘ 𝑈 ) } ) → 𝑋 ∈ 𝑆 )
32		simpr	⊢ ( ( 𝜑 ∧ 𝑋 ≠ { ( 0g ‘ 𝑈 ) } ) → 𝑋 ≠ { ( 0g ‘ 𝑈 ) } )
33	9	adantr	⊢ ( ( 𝜑 ∧ 𝑋 ≠ { ( 0g ‘ 𝑈 ) } ) → ( ⊥ ‘ ( ⊥ ‘ 𝑋 ) ) = 𝑋 )
34	1 2 3 4 5 28 6 29 30 31 14 32 33	dochexmidlem8	⊢ ( ( 𝜑 ∧ 𝑋 ≠ { ( 0g ‘ 𝑈 ) } ) → ( 𝑋 ⊕ ( ⊥ ‘ 𝑋 ) ) = 𝑉 )
35	27 34	pm2.61dane	⊢ ( 𝜑 → ( 𝑋 ⊕ ( ⊥ ‘ 𝑋 ) ) = 𝑉 )