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

Metamath Proof Explorer

Theorem omlsilem

Description: Lemma for orthomodular law in the Hilbert lattice. (Contributed by NM, 14-Oct-1999) (New usage is discouraged.)

Ref Expression
Hypotheses omlsilem.1 ⊢ G ∈ S ℋ
omlsilem.2 ⊢ H ∈ S ℋ
omlsilem.3 ⊢ G ⊆ H
omlsilem.4 ⊢ H ∩ ⊥ ⁡ G = 0 ℋ
omlsilem.5 ⊢ A ∈ H
omlsilem.6 ⊢ B ∈ G
omlsilem.7 ⊢ C ∈ ⊥ ⁡ G
Assertion omlsilem ⊢ A = B + ℎ C → A ∈ G

Proof

Step Hyp Ref Expression
1 omlsilem.1 ⊢ G ∈ S ℋ
2 omlsilem.2 ⊢ H ∈ S ℋ
3 omlsilem.3 ⊢ G ⊆ H
4 omlsilem.4 ⊢ H ∩ ⊥ ⁡ G = 0 ℋ
5 omlsilem.5 ⊢ A ∈ H
6 omlsilem.6 ⊢ B ∈ G
7 omlsilem.7 ⊢ C ∈ ⊥ ⁡ G
8 2 5 shelii ⊢ A ∈ ℋ
9 1 6 shelii ⊢ B ∈ ℋ
10 shocss ⊢ G ∈ S ℋ → ⊥ ⁡ G ⊆ ℋ
11 1 10 ax-mp ⊢ ⊥ ⁡ G ⊆ ℋ
12 11 7 sselii ⊢ C ∈ ℋ
13 8 9 12 hvsubaddi ⊢ A - ℎ B = C ↔ B + ℎ C = A
14 eqcom ⊢ B + ℎ C = A ↔ A = B + ℎ C
15 13 14 bitri ⊢ A - ℎ B = C ↔ A = B + ℎ C
16 3 6 sselii ⊢ B ∈ H
17 shsubcl ⊢ H ∈ S ℋ ∧ A ∈ H ∧ B ∈ H → A - ℎ B ∈ H
18 2 5 16 17 mp3an ⊢ A - ℎ B ∈ H
19 eleq1 ⊢ A - ℎ B = C → A - ℎ B ∈ H ↔ C ∈ H
20 18 19 mpbii ⊢ A - ℎ B = C → C ∈ H
21 15 20 sylbir ⊢ A = B + ℎ C → C ∈ H
22 4 eleq2i ⊢ C ∈ H ∩ ⊥ ⁡ G ↔ C ∈ 0 ℋ
23 elin ⊢ C ∈ H ∩ ⊥ ⁡ G ↔ C ∈ H ∧ C ∈ ⊥ ⁡ G
24 elch0 ⊢ C ∈ 0 ℋ ↔ C = 0 ℎ
25 22 23 24 3bitr3i ⊢ C ∈ H ∧ C ∈ ⊥ ⁡ G ↔ C = 0 ℎ
26 21 7 25 sylanblc ⊢ A = B + ℎ C → C = 0 ℎ
27 26 oveq2d ⊢ A = B + ℎ C → B + ℎ C = B + ℎ 0 ℎ
28 ax-hvaddid ⊢ B ∈ ℋ → B + ℎ 0 ℎ = B
29 9 28 ax-mp ⊢ B + ℎ 0 ℎ = B
30 27 29 eqtrdi ⊢ A = B + ℎ C → B + ℎ C = B
31 30 6 eqeltrdi ⊢ A = B + ℎ C → B + ℎ C ∈ G
32 eleq1 ⊢ A = B + ℎ C → A ∈ G ↔ B + ℎ C ∈ G
33 31 32 mpbird ⊢ A = B + ℎ C → A ∈ G