Theorem pexmidALTN 37118

Description: Excluded middle law for closed projective subspaces, which is equivalent to (and derived from) the orthomodular law poml4N 37093. Lemma 3.3(2) in [Holland95] p. 215. In our proof, we use the variables 𝑋, 𝑀, 𝑝, 𝑞, 𝑟 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.)

Hypotheses

Ref	Expression
pexmidALT.a	⊢ 𝐴 = (Atoms‘𝐾)
pexmidALT.p	⊢ + = (+𝑃‘𝐾)
pexmidALT.o	⊢ ⊥ = (⊥𝑃‘𝐾)

Assertion

Ref	Expression
pexmidALTN	⊢ (((𝐾 ∈ HL ∧ 𝑋 ⊆ 𝐴) ∧ ( ⊥ ‘( ⊥ ‘𝑋)) = 𝑋) → (𝑋 + ( ⊥ ‘𝑋)) = 𝐴)

Proof of Theorem pexmidALTN

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

Syntax hints:   → wi 4   ∧ wa 398   = wceq 1536   ∈ wcel 2113   ≠ wne 3019   ⊆ wss 3939  ∅c0 4294  ‘cfv 6358  (class class class)co 7159  Atomscatm 36403  HLchlt 36490  +_𝑃cpadd 36935  ⊥_𝑃cpolN 37042

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1969  ax-7 2014  ax-8 2115  ax-9 2123  ax-10 2144  ax-11 2160  ax-12 2176  ax-ext 2796  ax-rep 5193  ax-sep 5206  ax-nul 5213  ax-pow 5269  ax-pr 5333  ax-un 7464  ax-riotaBAD 36093

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-3an 1085  df-tru 1539  df-fal 1549  df-ex 1780  df-nf 1784  df-sb 2069  df-mo 2621  df-eu 2653  df-clab 2803  df-cleq 2817  df-clel 2896  df-nfc 2966  df-ne 3020  df-ral 3146  df-rex 3147  df-reu 3148  df-rmo 3149  df-rab 3150  df-v 3499  df-sbc 3776  df-csb 3887  df-dif 3942  df-un 3944  df-in 3946  df-ss 3955  df-pss 3957  df-nul 4295  df-if 4471  df-pw 4544  df-sn 4571  df-pr 4573  df-op 4577  df-uni 4842  df-iun 4924  df-iin 4925  df-br 5070  df-opab 5132  df-mpt 5150  df-id 5463  df-xp 5564  df-rel 5565  df-cnv 5566  df-co 5567  df-dm 5568  df-rn 5569  df-res 5570  df-ima 5571  df-iota 6317  df-fun 6360  df-fn 6361  df-f 6362  df-f1 6363  df-fo 6364  df-f1o 6365  df-fv 6366  df-riota 7117  df-ov 7162  df-oprab 7163  df-mpo 7164  df-1st 7692  df-2nd 7693  df-undef 7942  df-proset 17541  df-poset 17559  df-plt 17571  df-lub 17587  df-glb 17588  df-join 17589  df-meet 17590  df-p0 17652  df-p1 17653  df-lat 17659  df-clat 17721  df-oposet 36316  df-ol 36318  df-oml 36319  df-covers 36406  df-ats 36407  df-atl 36438  df-cvlat 36462  df-hlat 36491  df-psubsp 36643  df-pmap 36644  df-padd 36936  df-polarityN 37043  df-psubclN 37075

This theorem is referenced by: (None)