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

Metamath Proof Explorer

Theorem omlsii

Description: Subspace inference form of orthomodular law in the Hilbert lattice. (Contributed by NM, 14-Oct-1999) (Revised by Mario Carneiro, 15-May-2014) (New usage is discouraged.)

Ref Expression
Hypotheses omlsi.1 ⊢ 𝐴 ∈ Cℋ
omlsi.2 ⊢ 𝐵 ∈ Sℋ
omlsi.3 ⊢ 𝐴 ⊆ 𝐵
omlsi.4 ⊢ ( 𝐵 ∩ ( ⊥ ‘ 𝐴 ) ) = 0ℋ
Assertion omlsii 𝐴 = 𝐵

Proof

Step Hyp Ref Expression
1 omlsi.1 ⊢ 𝐴 ∈ Cℋ
2 omlsi.2 ⊢ 𝐵 ∈ Sℋ
3 omlsi.3 ⊢ 𝐴 ⊆ 𝐵
4 omlsi.4 ⊢ ( 𝐵 ∩ ( ⊥ ‘ 𝐴 ) ) = 0ℋ
5 2 sheli ⊢ ( 𝑥 ∈ 𝐵 → 𝑥 ∈ ℋ )
6 1 5 pjhthlem2 ⊢ ( 𝑥 ∈ 𝐵 → ∃ 𝑦 ∈ 𝐴 ∃ 𝑧 ∈ ( ⊥ ‘ 𝐴 ) 𝑥 = ( 𝑦 +ℎ 𝑧 ) )
7 eqeq1 ⊢ ( 𝑥 = if ( 𝑥 ∈ 𝐵 , 𝑥 , 0ℎ ) → ( 𝑥 = ( 𝑦 +ℎ 𝑧 ) ↔ if ( 𝑥 ∈ 𝐵 , 𝑥 , 0ℎ ) = ( 𝑦 +ℎ 𝑧 ) ) )
8 eleq1 ⊢ ( 𝑥 = if ( 𝑥 ∈ 𝐵 , 𝑥 , 0ℎ ) → ( 𝑥 ∈ 𝐴 ↔ if ( 𝑥 ∈ 𝐵 , 𝑥 , 0ℎ ) ∈ 𝐴 ) )
9 7 8 imbi12d ⊢ ( 𝑥 = if ( 𝑥 ∈ 𝐵 , 𝑥 , 0ℎ ) → ( ( 𝑥 = ( 𝑦 +ℎ 𝑧 ) → 𝑥 ∈ 𝐴 ) ↔ ( if ( 𝑥 ∈ 𝐵 , 𝑥 , 0ℎ ) = ( 𝑦 +ℎ 𝑧 ) → if ( 𝑥 ∈ 𝐵 , 𝑥 , 0ℎ ) ∈ 𝐴 ) ) )
10 oveq1 ⊢ ( 𝑦 = if ( 𝑦 ∈ 𝐴 , 𝑦 , 0ℎ ) → ( 𝑦 +ℎ 𝑧 ) = ( if ( 𝑦 ∈ 𝐴 , 𝑦 , 0ℎ ) +ℎ 𝑧 ) )
11 10 eqeq2d ⊢ ( 𝑦 = if ( 𝑦 ∈ 𝐴 , 𝑦 , 0ℎ ) → ( if ( 𝑥 ∈ 𝐵 , 𝑥 , 0ℎ ) = ( 𝑦 +ℎ 𝑧 ) ↔ if ( 𝑥 ∈ 𝐵 , 𝑥 , 0ℎ ) = ( if ( 𝑦 ∈ 𝐴 , 𝑦 , 0ℎ ) +ℎ 𝑧 ) ) )
12 11 imbi1d ⊢ ( 𝑦 = if ( 𝑦 ∈ 𝐴 , 𝑦 , 0ℎ ) → ( ( if ( 𝑥 ∈ 𝐵 , 𝑥 , 0ℎ ) = ( 𝑦 +ℎ 𝑧 ) → if ( 𝑥 ∈ 𝐵 , 𝑥 , 0ℎ ) ∈ 𝐴 ) ↔ ( if ( 𝑥 ∈ 𝐵 , 𝑥 , 0ℎ ) = ( if ( 𝑦 ∈ 𝐴 , 𝑦 , 0ℎ ) +ℎ 𝑧 ) → if ( 𝑥 ∈ 𝐵 , 𝑥 , 0ℎ ) ∈ 𝐴 ) ) )
13 oveq2 ⊢ ( 𝑧 = if ( 𝑧 ∈ ( ⊥ ‘ 𝐴 ) , 𝑧 , 0ℎ ) → ( if ( 𝑦 ∈ 𝐴 , 𝑦 , 0ℎ ) +ℎ 𝑧 ) = ( if ( 𝑦 ∈ 𝐴 , 𝑦 , 0ℎ ) +ℎ if ( 𝑧 ∈ ( ⊥ ‘ 𝐴 ) , 𝑧 , 0ℎ ) ) )
14 13 eqeq2d ⊢ ( 𝑧 = if ( 𝑧 ∈ ( ⊥ ‘ 𝐴 ) , 𝑧 , 0ℎ ) → ( if ( 𝑥 ∈ 𝐵 , 𝑥 , 0ℎ ) = ( if ( 𝑦 ∈ 𝐴 , 𝑦 , 0ℎ ) +ℎ 𝑧 ) ↔ if ( 𝑥 ∈ 𝐵 , 𝑥 , 0ℎ ) = ( if ( 𝑦 ∈ 𝐴 , 𝑦 , 0ℎ ) +ℎ if ( 𝑧 ∈ ( ⊥ ‘ 𝐴 ) , 𝑧 , 0ℎ ) ) ) )
15 14 imbi1d ⊢ ( 𝑧 = if ( 𝑧 ∈ ( ⊥ ‘ 𝐴 ) , 𝑧 , 0ℎ ) → ( ( if ( 𝑥 ∈ 𝐵 , 𝑥 , 0ℎ ) = ( if ( 𝑦 ∈ 𝐴 , 𝑦 , 0ℎ ) +ℎ 𝑧 ) → if ( 𝑥 ∈ 𝐵 , 𝑥 , 0ℎ ) ∈ 𝐴 ) ↔ ( if ( 𝑥 ∈ 𝐵 , 𝑥 , 0ℎ ) = ( if ( 𝑦 ∈ 𝐴 , 𝑦 , 0ℎ ) +ℎ if ( 𝑧 ∈ ( ⊥ ‘ 𝐴 ) , 𝑧 , 0ℎ ) ) → if ( 𝑥 ∈ 𝐵 , 𝑥 , 0ℎ ) ∈ 𝐴 ) ) )
16 1 chshii ⊢ 𝐴 ∈ Sℋ
17 sh0 ⊢ ( 𝐵 ∈ Sℋ → 0ℎ ∈ 𝐵 )
18 2 17 ax-mp ⊢ 0ℎ ∈ 𝐵
19 18 elimel ⊢ if ( 𝑥 ∈ 𝐵 , 𝑥 , 0ℎ ) ∈ 𝐵
20 ch0 ⊢ ( 𝐴 ∈ Cℋ → 0ℎ ∈ 𝐴 )
21 1 20 ax-mp ⊢ 0ℎ ∈ 𝐴
22 21 elimel ⊢ if ( 𝑦 ∈ 𝐴 , 𝑦 , 0ℎ ) ∈ 𝐴
23 shocsh ⊢ ( 𝐴 ∈ Sℋ → ( ⊥ ‘ 𝐴 ) ∈ Sℋ )
24 16 23 ax-mp ⊢ ( ⊥ ‘ 𝐴 ) ∈ Sℋ
25 sh0 ⊢ ( ( ⊥ ‘ 𝐴 ) ∈ Sℋ → 0ℎ ∈ ( ⊥ ‘ 𝐴 ) )
26 24 25 ax-mp ⊢ 0ℎ ∈ ( ⊥ ‘ 𝐴 )
27 26 elimel ⊢ if ( 𝑧 ∈ ( ⊥ ‘ 𝐴 ) , 𝑧 , 0ℎ ) ∈ ( ⊥ ‘ 𝐴 )
28 16 2 3 4 19 22 27 omlsilem ⊢ ( if ( 𝑥 ∈ 𝐵 , 𝑥 , 0ℎ ) = ( if ( 𝑦 ∈ 𝐴 , 𝑦 , 0ℎ ) +ℎ if ( 𝑧 ∈ ( ⊥ ‘ 𝐴 ) , 𝑧 , 0ℎ ) ) → if ( 𝑥 ∈ 𝐵 , 𝑥 , 0ℎ ) ∈ 𝐴 )
29 9 12 15 28 dedth3h ⊢ ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐴 ∧ 𝑧 ∈ ( ⊥ ‘ 𝐴 ) ) → ( 𝑥 = ( 𝑦 +ℎ 𝑧 ) → 𝑥 ∈ 𝐴 ) )
30 29 3expia ⊢ ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐴 ) → ( 𝑧 ∈ ( ⊥ ‘ 𝐴 ) → ( 𝑥 = ( 𝑦 +ℎ 𝑧 ) → 𝑥 ∈ 𝐴 ) ) )
31 30 rexlimdv ⊢ ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐴 ) → ( ∃ 𝑧 ∈ ( ⊥ ‘ 𝐴 ) 𝑥 = ( 𝑦 +ℎ 𝑧 ) → 𝑥 ∈ 𝐴 ) )
32 31 rexlimdva ⊢ ( 𝑥 ∈ 𝐵 → ( ∃ 𝑦 ∈ 𝐴 ∃ 𝑧 ∈ ( ⊥ ‘ 𝐴 ) 𝑥 = ( 𝑦 +ℎ 𝑧 ) → 𝑥 ∈ 𝐴 ) )
33 6 32 mpd ⊢ ( 𝑥 ∈ 𝐵 → 𝑥 ∈ 𝐴 )
34 33 ssriv ⊢ 𝐵 ⊆ 𝐴
35 3 34 eqssi ⊢ 𝐴 = 𝐵