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	⊢ 𝐴 = ( Atoms ‘ 𝐾 )
	pexmidALT.p	⊢ + = ( +𝑃 ‘ 𝐾 )
	pexmidALT.o	⊢ ⊥ = ( ⊥𝑃 ‘ 𝐾 )
Assertion	pexmidALTN	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ⊆ 𝐴 ) ∧ ( ⊥ ‘ ( ⊥ ‘ 𝑋 ) ) = 𝑋 ) → ( 𝑋 + ( ⊥ ‘ 𝑋 ) ) = 𝐴 )

Proof

Step	Hyp	Ref	Expression
1		pexmidALT.a	⊢ 𝐴 = ( Atoms ‘ 𝐾 )
2		pexmidALT.p	⊢ + = ( +𝑃 ‘ 𝐾 )
3		pexmidALT.o	⊢ ⊥ = ( ⊥𝑃 ‘ 𝐾 )
4		id	⊢ ( 𝑋 = ∅ → 𝑋 = ∅ )
5		fveq2	⊢ ( 𝑋 = ∅ → ( ⊥ ‘ 𝑋 ) = ( ⊥ ‘ ∅ ) )
6	4 5	oveq12d	⊢ ( 𝑋 = ∅ → ( 𝑋 + ( ⊥ ‘ 𝑋 ) ) = ( ∅ + ( ⊥ ‘ ∅ ) ) )
7	1 3	pol0N	⊢ ( 𝐾 ∈ HL → ( ⊥ ‘ ∅ ) = 𝐴 )
8		eqimss	⊢ ( ( ⊥ ‘ ∅ ) = 𝐴 → ( ⊥ ‘ ∅ ) ⊆ 𝐴 )
9	7 8	syl	⊢ ( 𝐾 ∈ HL → ( ⊥ ‘ ∅ ) ⊆ 𝐴 )
10	1 2	padd02	⊢ ( ( 𝐾 ∈ HL ∧ ( ⊥ ‘ ∅ ) ⊆ 𝐴 ) → ( ∅ + ( ⊥ ‘ ∅ ) ) = ( ⊥ ‘ ∅ ) )
11	9 10	mpdan	⊢ ( 𝐾 ∈ HL → ( ∅ + ( ⊥ ‘ ∅ ) ) = ( ⊥ ‘ ∅ ) )
12	11 7	eqtrd	⊢ ( 𝐾 ∈ HL → ( ∅ + ( ⊥ ‘ ∅ ) ) = 𝐴 )
13	12	ad2antrr	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ⊆ 𝐴 ) ∧ ( ⊥ ‘ ( ⊥ ‘ 𝑋 ) ) = 𝑋 ) → ( ∅ + ( ⊥ ‘ ∅ ) ) = 𝐴 )
14	6 13	sylan9eqr	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑋 ⊆ 𝐴 ) ∧ ( ⊥ ‘ ( ⊥ ‘ 𝑋 ) ) = 𝑋 ) ∧ 𝑋 = ∅ ) → ( 𝑋 + ( ⊥ ‘ 𝑋 ) ) = 𝐴 )
15	1 2 3	pexmidlem8N	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ⊆ 𝐴 ) ∧ ( ( ⊥ ‘ ( ⊥ ‘ 𝑋 ) ) = 𝑋 ∧ 𝑋 ≠ ∅ ) ) → ( 𝑋 + ( ⊥ ‘ 𝑋 ) ) = 𝐴 )
16	15	anassrs	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑋 ⊆ 𝐴 ) ∧ ( ⊥ ‘ ( ⊥ ‘ 𝑋 ) ) = 𝑋 ) ∧ 𝑋 ≠ ∅ ) → ( 𝑋 + ( ⊥ ‘ 𝑋 ) ) = 𝐴 )
17	14 16	pm2.61dane	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ⊆ 𝐴 ) ∧ ( ⊥ ‘ ( ⊥ ‘ 𝑋 ) ) = 𝑋 ) → ( 𝑋 + ( ⊥ ‘ 𝑋 ) ) = 𝐴 )