Theorem isoml 37238

Description: The predicate "is an orthomodular lattice." (Contributed by NM, 18-Sep-2011.)

Hypotheses

Ref	Expression
isoml.b	⊢ 𝐵 = (Base‘𝐾)
isoml.l	⊢ ≤ = (le‘𝐾)
isoml.j	⊢ ∨ = (join‘𝐾)
isoml.m	⊢ ∧ = (meet‘𝐾)
isoml.o	⊢ ⊥ = (oc‘𝐾)

Assertion

Ref	Expression
isoml	⊢ (𝐾 ∈ OML ↔ (𝐾 ∈ OL ∧ ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 (𝑥 ≤ 𝑦 → 𝑦 = (𝑥 ∨ (𝑦 ∧ ( ⊥ ‘𝑥))))))

Distinct variable groups:   𝑥,𝑦,𝐵   𝑥,𝐾,𝑦

Allowed substitution hints:   ∨ (𝑥,𝑦)   ≤ (𝑥,𝑦)   ∧ (𝑥,𝑦)   ⊥ (𝑥,𝑦)

Proof of Theorem isoml

Dummy variable 𝑘 is distinct from all other variables.

Step	Hyp	Ref	Expression
1		fveq2 6767	. . . 4 ⊢ (𝑘 = 𝐾 → (Base‘𝑘) = (Base‘𝐾))
2		isoml.b	. . . 4 ⊢ 𝐵 = (Base‘𝐾)
3	1, 2	eqtr4di 2796	. . 3 ⊢ (𝑘 = 𝐾 → (Base‘𝑘) = 𝐵)
4		fveq2 6767	. . . . . . 7 ⊢ (𝑘 = 𝐾 → (le‘𝑘) = (le‘𝐾))
5		isoml.l	. . . . . . 7 ⊢ ≤ = (le‘𝐾)
6	4, 5	eqtr4di 2796	. . . . . 6 ⊢ (𝑘 = 𝐾 → (le‘𝑘) = ≤ )
7	6	breqd 5085	. . . . 5 ⊢ (𝑘 = 𝐾 → (𝑥(le‘𝑘)𝑦 ↔ 𝑥 ≤ 𝑦))
8		fveq2 6767	. . . . . . . 8 ⊢ (𝑘 = 𝐾 → (join‘𝑘) = (join‘𝐾))
9		isoml.j	. . . . . . . 8 ⊢ ∨ = (join‘𝐾)
10	8, 9	eqtr4di 2796	. . . . . . 7 ⊢ (𝑘 = 𝐾 → (join‘𝑘) = ∨ )
11		eqidd 2739	. . . . . . 7 ⊢ (𝑘 = 𝐾 → 𝑥 = 𝑥)
12		fveq2 6767	. . . . . . . . 9 ⊢ (𝑘 = 𝐾 → (meet‘𝑘) = (meet‘𝐾))
13		isoml.m	. . . . . . . . 9 ⊢ ∧ = (meet‘𝐾)
14	12, 13	eqtr4di 2796	. . . . . . . 8 ⊢ (𝑘 = 𝐾 → (meet‘𝑘) = ∧ )
15		eqidd 2739	. . . . . . . 8 ⊢ (𝑘 = 𝐾 → 𝑦 = 𝑦)
16		fveq2 6767	. . . . . . . . . 10 ⊢ (𝑘 = 𝐾 → (oc‘𝑘) = (oc‘𝐾))
17		isoml.o	. . . . . . . . . 10 ⊢ ⊥ = (oc‘𝐾)
18	16, 17	eqtr4di 2796	. . . . . . . . 9 ⊢ (𝑘 = 𝐾 → (oc‘𝑘) = ⊥ )
19	18	fveq1d 6769	. . . . . . . 8 ⊢ (𝑘 = 𝐾 → ((oc‘𝑘)‘𝑥) = ( ⊥ ‘𝑥))
20	14, 15, 19	oveq123d 7289	. . . . . . 7 ⊢ (𝑘 = 𝐾 → (𝑦(meet‘𝑘)((oc‘𝑘)‘𝑥)) = (𝑦 ∧ ( ⊥ ‘𝑥)))
21	10, 11, 20	oveq123d 7289	. . . . . 6 ⊢ (𝑘 = 𝐾 → (𝑥(join‘𝑘)(𝑦(meet‘𝑘)((oc‘𝑘)‘𝑥))) = (𝑥 ∨ (𝑦 ∧ ( ⊥ ‘𝑥))))
22	21	eqeq2d 2749	. . . . 5 ⊢ (𝑘 = 𝐾 → (𝑦 = (𝑥(join‘𝑘)(𝑦(meet‘𝑘)((oc‘𝑘)‘𝑥))) ↔ 𝑦 = (𝑥 ∨ (𝑦 ∧ ( ⊥ ‘𝑥)))))
23	7, 22	imbi12d 345	. . . 4 ⊢ (𝑘 = 𝐾 → ((𝑥(le‘𝑘)𝑦 → 𝑦 = (𝑥(join‘𝑘)(𝑦(meet‘𝑘)((oc‘𝑘)‘𝑥)))) ↔ (𝑥 ≤ 𝑦 → 𝑦 = (𝑥 ∨ (𝑦 ∧ ( ⊥ ‘𝑥))))))
24	3, 23	raleqbidv 3334	. . 3 ⊢ (𝑘 = 𝐾 → (∀𝑦 ∈ (Base‘𝑘)(𝑥(le‘𝑘)𝑦 → 𝑦 = (𝑥(join‘𝑘)(𝑦(meet‘𝑘)((oc‘𝑘)‘𝑥)))) ↔ ∀𝑦 ∈ 𝐵 (𝑥 ≤ 𝑦 → 𝑦 = (𝑥 ∨ (𝑦 ∧ ( ⊥ ‘𝑥))))))
25	3, 24	raleqbidv 3334	. 2 ⊢ (𝑘 = 𝐾 → (∀𝑥 ∈ (Base‘𝑘)∀𝑦 ∈ (Base‘𝑘)(𝑥(le‘𝑘)𝑦 → 𝑦 = (𝑥(join‘𝑘)(𝑦(meet‘𝑘)((oc‘𝑘)‘𝑥)))) ↔ ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 (𝑥 ≤ 𝑦 → 𝑦 = (𝑥 ∨ (𝑦 ∧ ( ⊥ ‘𝑥))))))
26		df-oml 37179	. 2 ⊢ OML = {𝑘 ∈ OL ∣ ∀𝑥 ∈ (Base‘𝑘)∀𝑦 ∈ (Base‘𝑘)(𝑥(le‘𝑘)𝑦 → 𝑦 = (𝑥(join‘𝑘)(𝑦(meet‘𝑘)((oc‘𝑘)‘𝑥))))}
27	25, 26	elrab2 3627	1 ⊢ (𝐾 ∈ OML ↔ (𝐾 ∈ OL ∧ ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 (𝑥 ≤ 𝑦 → 𝑦 = (𝑥 ∨ (𝑦 ∧ ( ⊥ ‘𝑥))))))

Syntax hints:   → wi 4   ↔ wb 205   ∧ wa 396   = wceq 1539   ∈ wcel 2106  ∀wral 3064   class class class wbr 5074  ‘cfv 6427  (class class class)co 7268  Basecbs 16900  lecple 16957  occoc 16958  joincjn 18017  meetcmee 18018  OLcol 37174  OMLcoml 37175

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-3an 1088  df-tru 1542  df-fal 1552  df-ex 1783  df-sb 2068  df-clab 2716  df-cleq 2730  df-clel 2816  df-ral 3069  df-rab 3073  df-v 3432  df-dif 3890  df-un 3892  df-in 3894  df-ss 3904  df-nul 4258  df-if 4461  df-sn 4563  df-pr 4565  df-op 4569  df-uni 4841  df-br 5075  df-iota 6385  df-fv 6435  df-ov 7271  df-oml 37179

This theorem is referenced by:  isomliN  37239  omlol  37240  omllaw  37243