Theorem pexmidALTN

Description: Excluded middle law for closed projective subspaces, which is equivalent to (and derived from) the orthomodular law poml4N . 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. TODO: should we make this obsolete? (Contributed by NM, 3-Feb-2012) (New usage is discouraged.)

	Ref	Expression
Hypotheses	pexmidALT.a	|- A = ( Atoms ` K )
	pexmidALT.p	|- .+ = ( +P ` K )
	pexmidALT.o	|- ._|_ = ( _|_P ` K )
Assertion	pexmidALTN	|- ( ( ( K e. HL /\ X C_ A ) /\ ( ._|_ ` ( ._|_ ` X ) ) = X ) -> ( X .+ ( ._|_ ` X ) ) = A )

Proof

Step	Hyp	Ref	Expression
1		pexmidALT.a	|- A = ( Atoms ` K )
2		pexmidALT.p	|- .+ = ( +P ` K )
3		pexmidALT.o	|- ._|_ = ( _|_P ` K )
4		id	|- ( X = (/) -> X = (/) )
5		fveq2	|- ( X = (/) -> ( ._|_ ` X ) = ( ._|_ ` (/) ) )
6	4 5	oveq12d	|- ( X = (/) -> ( X .+ ( ._|_ ` X ) ) = ( (/) .+ ( ._|_ ` (/) ) ) )
7	1 3	pol0N	|- ( K e. HL -> ( ._|_ ` (/) ) = A )
8		eqimss	|- ( ( ._|_ ` (/) ) = A -> ( ._|_ ` (/) ) C_ A )
9	7 8	syl	|- ( K e. HL -> ( ._|_ ` (/) ) C_ A )
10	1 2	padd02	|- ( ( K e. HL /\ ( ._|_ ` (/) ) C_ A ) -> ( (/) .+ ( ._|_ ` (/) ) ) = ( ._|_ ` (/) ) )
11	9 10	mpdan	|- ( K e. HL -> ( (/) .+ ( ._|_ ` (/) ) ) = ( ._|_ ` (/) ) )
12	11 7	eqtrd	|- ( K e. HL -> ( (/) .+ ( ._|_ ` (/) ) ) = A )
13	12	ad2antrr	|- ( ( ( K e. HL /\ X C_ A ) /\ ( ._|_ ` ( ._|_ ` X ) ) = X ) -> ( (/) .+ ( ._|_ ` (/) ) ) = A )
14	6 13	sylan9eqr	|- ( ( ( ( K e. HL /\ X C_ A ) /\ ( ._|_ ` ( ._|_ ` X ) ) = X ) /\ X = (/) ) -> ( X .+ ( ._|_ ` X ) ) = A )
15	1 2 3	pexmidlem8N	|- ( ( ( K e. HL /\ X C_ A ) /\ ( ( ._|_ ` ( ._|_ ` X ) ) = X /\ X =/= (/) ) ) -> ( X .+ ( ._|_ ` X ) ) = A )
16	15	anassrs	|- ( ( ( ( K e. HL /\ X C_ A ) /\ ( ._|_ ` ( ._|_ ` X ) ) = X ) /\ X =/= (/) ) -> ( X .+ ( ._|_ ` X ) ) = A )
17	14 16	pm2.61dane	|- ( ( ( K e. HL /\ X C_ A ) /\ ( ._|_ ` ( ._|_ ` X ) ) = X ) -> ( X .+ ( ._|_ ` X ) ) = A )