This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ⊢ ( 𝜑 → ( 𝑋 ⊕ ( ⊥ ‘ 𝑋 ) ) = 𝑉 )