Metamath Proof Explorer

Theorem pexmidN

Description: Excluded middle law for closed projective subspaces, which can be shown to be equivalent to (and derivable from) the orthomodular law poml4N . Lemma 3.3(2) in Holland95 p. 215, which we prove as a special case of osumclN . (Contributed by NM, 25-Mar-2012) (New usage is discouraged.)

Ref Expression
Hypotheses pexmid.a ⊢ 𝐴 = ( Atoms ‘ 𝐾 )
pexmid.p ⊢ + = ( +𝑃 ‘ 𝐾 )
pexmid.o ⊢ ⊥ = ( ⊥𝑃 ‘ 𝐾 )
Assertion pexmidN ( ( ( 𝐾 ∈ HL ∧ 𝑋 ⊆ 𝐴 ) ∧ ( ⊥ ‘ ( ⊥ ‘ 𝑋 ) ) = 𝑋 ) → ( 𝑋 + ( ⊥ ‘ 𝑋 ) ) = 𝐴 )

Proof

Step Hyp Ref Expression
1 pexmid.a ⊢ 𝐴 = ( Atoms ‘ 𝐾 )
2 pexmid.p ⊢ + = ( +𝑃 ‘ 𝐾 )
3 pexmid.o ⊢ ⊥ = ( ⊥𝑃 ‘ 𝐾 )
4 simpll ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ⊆ 𝐴 ) ∧ ( ⊥ ‘ ( ⊥ ‘ 𝑋 ) ) = 𝑋 ) → 𝐾 ∈ HL )
5 simplr ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ⊆ 𝐴 ) ∧ ( ⊥ ‘ ( ⊥ ‘ 𝑋 ) ) = 𝑋 ) → 𝑋 ⊆ 𝐴 )
6 1 3 polssatN ⊢ ( ( 𝐾 ∈ HL ∧ 𝑋 ⊆ 𝐴 ) → ( ⊥ ‘ 𝑋 ) ⊆ 𝐴 )
7 6 adantr ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ⊆ 𝐴 ) ∧ ( ⊥ ‘ ( ⊥ ‘ 𝑋 ) ) = 𝑋 ) → ( ⊥ ‘ 𝑋 ) ⊆ 𝐴 )
8 1 2 3 poldmj1N ⊢ ( ( 𝐾 ∈ HL ∧ 𝑋 ⊆ 𝐴 ∧ ( ⊥ ‘ 𝑋 ) ⊆ 𝐴 ) → ( ⊥ ‘ ( 𝑋 + ( ⊥ ‘ 𝑋 ) ) ) = ( ( ⊥ ‘ 𝑋 ) ∩ ( ⊥ ‘ ( ⊥ ‘ 𝑋 ) ) ) )
9 4 5 7 8 syl3anc ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ⊆ 𝐴 ) ∧ ( ⊥ ‘ ( ⊥ ‘ 𝑋 ) ) = 𝑋 ) → ( ⊥ ‘ ( 𝑋 + ( ⊥ ‘ 𝑋 ) ) ) = ( ( ⊥ ‘ 𝑋 ) ∩ ( ⊥ ‘ ( ⊥ ‘ 𝑋 ) ) ) )
10 1 3 pnonsingN ⊢ ( ( 𝐾 ∈ HL ∧ ( ⊥ ‘ 𝑋 ) ⊆ 𝐴 ) → ( ( ⊥ ‘ 𝑋 ) ∩ ( ⊥ ‘ ( ⊥ ‘ 𝑋 ) ) ) = ∅ )
11 4 7 10 syl2anc ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ⊆ 𝐴 ) ∧ ( ⊥ ‘ ( ⊥ ‘ 𝑋 ) ) = 𝑋 ) → ( ( ⊥ ‘ 𝑋 ) ∩ ( ⊥ ‘ ( ⊥ ‘ 𝑋 ) ) ) = ∅ )
12 9 11 eqtrd ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ⊆ 𝐴 ) ∧ ( ⊥ ‘ ( ⊥ ‘ 𝑋 ) ) = 𝑋 ) → ( ⊥ ‘ ( 𝑋 + ( ⊥ ‘ 𝑋 ) ) ) = ∅ )
13 12 fveq2d ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ⊆ 𝐴 ) ∧ ( ⊥ ‘ ( ⊥ ‘ 𝑋 ) ) = 𝑋 ) → ( ⊥ ‘ ( ⊥ ‘ ( 𝑋 + ( ⊥ ‘ 𝑋 ) ) ) ) = ( ⊥ ‘ ∅ ) )
14 simpr ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ⊆ 𝐴 ) ∧ ( ⊥ ‘ ( ⊥ ‘ 𝑋 ) ) = 𝑋 ) → ( ⊥ ‘ ( ⊥ ‘ 𝑋 ) ) = 𝑋 )
15 eqid ⊢ ( PSubCl ‘ 𝐾 ) = ( PSubCl ‘ 𝐾 )
16 1 3 15 ispsubclN ⊢ ( 𝐾 ∈ HL → ( 𝑋 ∈ ( PSubCl ‘ 𝐾 ) ↔ ( 𝑋 ⊆ 𝐴 ∧ ( ⊥ ‘ ( ⊥ ‘ 𝑋 ) ) = 𝑋 ) ) )
17 16 ad2antrr ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ⊆ 𝐴 ) ∧ ( ⊥ ‘ ( ⊥ ‘ 𝑋 ) ) = 𝑋 ) → ( 𝑋 ∈ ( PSubCl ‘ 𝐾 ) ↔ ( 𝑋 ⊆ 𝐴 ∧ ( ⊥ ‘ ( ⊥ ‘ 𝑋 ) ) = 𝑋 ) ) )
18 5 14 17 mpbir2and ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ⊆ 𝐴 ) ∧ ( ⊥ ‘ ( ⊥ ‘ 𝑋 ) ) = 𝑋 ) → 𝑋 ∈ ( PSubCl ‘ 𝐾 ) )
19 1 3 15 polsubclN ⊢ ( ( 𝐾 ∈ HL ∧ 𝑋 ⊆ 𝐴 ) → ( ⊥ ‘ 𝑋 ) ∈ ( PSubCl ‘ 𝐾 ) )
20 19 adantr ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ⊆ 𝐴 ) ∧ ( ⊥ ‘ ( ⊥ ‘ 𝑋 ) ) = 𝑋 ) → ( ⊥ ‘ 𝑋 ) ∈ ( PSubCl ‘ 𝐾 ) )
21 1 3 2polssN ⊢ ( ( 𝐾 ∈ HL ∧ 𝑋 ⊆ 𝐴 ) → 𝑋 ⊆ ( ⊥ ‘ ( ⊥ ‘ 𝑋 ) ) )
22 21 adantr ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ⊆ 𝐴 ) ∧ ( ⊥ ‘ ( ⊥ ‘ 𝑋 ) ) = 𝑋 ) → 𝑋 ⊆ ( ⊥ ‘ ( ⊥ ‘ 𝑋 ) ) )
23 2 3 15 osumclN ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ ( PSubCl ‘ 𝐾 ) ∧ ( ⊥ ‘ 𝑋 ) ∈ ( PSubCl ‘ 𝐾 ) ) ∧ 𝑋 ⊆ ( ⊥ ‘ ( ⊥ ‘ 𝑋 ) ) ) → ( 𝑋 + ( ⊥ ‘ 𝑋 ) ) ∈ ( PSubCl ‘ 𝐾 ) )
24 4 18 20 22 23 syl31anc ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ⊆ 𝐴 ) ∧ ( ⊥ ‘ ( ⊥ ‘ 𝑋 ) ) = 𝑋 ) → ( 𝑋 + ( ⊥ ‘ 𝑋 ) ) ∈ ( PSubCl ‘ 𝐾 ) )
25 3 15 psubcli2N ⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑋 + ( ⊥ ‘ 𝑋 ) ) ∈ ( PSubCl ‘ 𝐾 ) ) → ( ⊥ ‘ ( ⊥ ‘ ( 𝑋 + ( ⊥ ‘ 𝑋 ) ) ) ) = ( 𝑋 + ( ⊥ ‘ 𝑋 ) ) )
26 4 24 25 syl2anc ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ⊆ 𝐴 ) ∧ ( ⊥ ‘ ( ⊥ ‘ 𝑋 ) ) = 𝑋 ) → ( ⊥ ‘ ( ⊥ ‘ ( 𝑋 + ( ⊥ ‘ 𝑋 ) ) ) ) = ( 𝑋 + ( ⊥ ‘ 𝑋 ) ) )
27 1 3 pol0N ⊢ ( 𝐾 ∈ HL → ( ⊥ ‘ ∅ ) = 𝐴 )
28 27 ad2antrr ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ⊆ 𝐴 ) ∧ ( ⊥ ‘ ( ⊥ ‘ 𝑋 ) ) = 𝑋 ) → ( ⊥ ‘ ∅ ) = 𝐴 )
29 13 26 28 3eqtr3d ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ⊆ 𝐴 ) ∧ ( ⊥ ‘ ( ⊥ ‘ 𝑋 ) ) = 𝑋 ) → ( 𝑋 + ( ⊥ ‘ 𝑋 ) ) = 𝐴 )