Theorem olj01 17881

Description: An ortholattice element joined with zero equals itself. (Th. chj0 12045 analog.)

Hypotheses

Ref	Expression
olj0.b	|- B = (Base` K)
olj0.j	|- ∨ = (join` K)
olj0.z	|- Z = (0.` K)

Assertion

Ref	Expression
olj01	|- ((K e. OL /\ X e. B) -> (X ∨ Z) = X)

Proof of Theorem olj01

Step	Hyp	Ref	Expression
1		olop 17870	. . . 4 |- (K e. OL -> K e. OP)
2		olj0.b	. . . . 5 |- B = (Base` K)
3		olj0.z	. . . . 5 |- Z = (0.` K)
4	2, 3	op0cl 17841	. . . 4 |- (K e. OP -> Z e. B)
5	1, 4	syl 13	. . 3 |- (K e. OL -> Z e. B)
6	5	adantr 543	. 2 |- ((K e. OL /\ X e. B) -> Z e. B)
7		eqid 2170	. . 3 |- (le` K) = (le` K)
8		ollat 17869	. . . 4 |- (K e. OL -> K e. Lat)
9	8	3ad2ant1 1169	. . 3 |- ((K e. OL /\ X e. B /\ Z e. B) -> K e. Lat)
10		olj0.j	. . . . 5 |- ∨ = (join` K)
11	2, 10	latjcl 9762	. . . 4 |- ((K e. Lat /\ X e. B /\ Z e. B) -> (X ∨ Z) e. B)
12	8, 11	syl3an1 1410	. . 3 |- ((K e. OL /\ X e. B /\ Z e. B) -> (X ∨ Z) e. B)
13		simp2 1149	. . 3 |- ((K e. OL /\ X e. B /\ Z e. B) -> X e. B)
14		simp3 1150	. . . . 5 |- ((K e. OL /\ X e. B /\ Z e. B) -> Z e. B)
15	2, 7, 10	latjle12 9774	. . . . 5 |- ((K e. Lat /\ (X e. B /\ Z e. B /\ X e. B)) -> ((X(le` K)X /\ Z(le` K)X) <-> (X ∨ Z)(le` K)X))
16	9, 13, 14, 13, 15	syl13anc 1379	. . . 4 |- ((K e. OL /\ X e. B /\ Z e. B) -> ((X(le` K)X /\ Z(le` K)X) <-> (X ∨ Z)(le` K)X))
17	2, 7	latref 9765	. . . . . 6 |- ((K e. Lat /\ X e. B) -> X(le` K)X)
18	8, 17	sylan 693	. . . . 5 |- ((K e. OL /\ X e. B) -> X(le` K)X)
19	18	3adant3 1168	. . . 4 |- ((K e. OL /\ X e. B /\ Z e. B) -> X(le` K)X)
20	2, 7, 3	op0le 17843	. . . . . 6 |- ((K e. OP /\ X e. B) -> Z(le` K)X)
21	1, 20	sylan 693	. . . . 5 |- ((K e. OL /\ X e. B) -> Z(le` K)X)
22	21	3adant3 1168	. . . 4 |- ((K e. OL /\ X e. B /\ Z e. B) -> Z(le` K)X)
23	16, 19, 22	mpbi2and 1063	. . 3 |- ((K e. OL /\ X e. B /\ Z e. B) -> (X ∨ Z)(le` K)X)
24	2, 7, 10	latlej1 9772	. . . 4 |- ((K e. Lat /\ X e. B /\ Z e. B) -> X(le` K)(X ∨ Z))
25	8, 24	syl3an1 1410	. . 3 |- ((K e. OL /\ X e. B /\ Z e. B) -> X(le` K)(X ∨ Z))
26	2, 7, 9, 12, 13, 23, 25	latasymd 9769	. 2 |- ((K e. OL /\ X e. B /\ Z e. B) -> (X ∨ Z) = X)
27	6, 26	mpd3an3 1495	1 |- ((K e. OL /\ X e. B) -> (X ∨ Z) = X)

Syntax hints:   -> wi 3   <-> wb 231   /\ wa 433   /\ w3a 1130   = wceq 1615   e. wcel 1617   class class class wbr 3539  ` cfv 4163  (class class class)co 5020  Basecbs 9579  lecple 9687  joincjn 9692  0.cp0 9749  Latclat 9751  OPcops 17828  OLcol 17830

This theorem is referenced by:  olj02 17882  olm11 17883  omllaw3 17901  2atm0atz 18226  2atm0atzOLD 18229  cdlemc6 18863  cdleme3c 18897  cdleme7e 18914  cdlemednpq 18966  cdlemefrs29pre00 19065  cdlemefrs29bpre0 19066  cdlemefrs29cpre1 19068  cdlemefrs32fva 19070  cdleme32fva 19108  cdleme42ke 19160  cdlemg0or 19320  cdlemg12e 19325  cdlemg31d 19378

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 1621  ax-gen 1622  ax-8 1623  ax-9 1624  ax-10 1625  ax-11 1626  ax-12 1627  ax-13 1628  ax-14 1629  ax-17 1634  ax-4 1637  ax-5o 1639  ax-6o 1642  ax-9o 1792  ax-10o 1810  ax-16 1883  ax-11o 1893  ax-ext 2152  ax-rep 3628  ax-sep 3638  ax-nul 3645  ax-pow 3681  ax-pr 3719  ax-un 3961

This theorem depends on definitions:  df-bi 232  df-or 434  df-an 435  df-3an 1132  df-ex 1645  df-sb 1845  df-eu 2070  df-mo 2071  df-clab 2158  df-cleq 2163  df-clel 2166  df-ne 2297  df-ral 2389  df-rex 2390  df-reu 2391  df-rab 2392  df-v 2571  df-sbc 2731  df-csb 2806  df-dif 2862  df-un 2864  df-in 2866  df-ss 2868  df-nul 3115  df-if 3213  df-pw 3261  df-sn 3274  df-pr 3275  df-op 3278  df-uni 3399  df-br 3540  df-opab 3598  df-id 3779  df-xp 4165  df-rel 4166  df-cnv 4167  df-co 4168  df-dm 4169  df-rn 4170  df-res 4171  df-ima 4172  df-fun 4173  df-fn 4174  df-f 4175  df-f1 4176  df-fo 4177  df-f1o 4178  df-fv 4179  df-opr 5022  df-oprab 5023  df-mpt 5138  df-mpt2 5139  df-iota 5259  df-er 5519  df-en 5631  df-dom 5632  df-sdom 5633  df-undef 5769  df-riota 5773  df-poset 9697  df-lub 9718  df-glb 9719  df-join 9720  df-p0 9752  df-lat 9758  df-oposet 17833  df-ol 17835

Copyright terms: Public domain