Theorem olm11

Description: The meet of an ortholattice element with one equals itself. ( chm1i analog.) (Contributed by NM, 22-May-2012)

	Ref	Expression
Hypotheses	olm1.b	$$⊢B={\mathrm{Base}}_K$$
	olm1.m	$$⊢\underset{\dot{}}{\wedge }=\mathrm{meet}\left(K\right)$$
	olm1.u	$$⊢\underset{\dot{}}{1}=\mathrm{1.}\left(K\right)$$
Assertion	olm11	$$⊢\left(K\in \mathrm{OL}\wedge X\in B\right)\to X\underset{\dot{}}{\wedge }\underset{\dot{}}{1}=X$$

Proof

Step	Hyp	Ref	Expression
1		olm1.b	$$⊢B={\mathrm{Base}}_K$$
2		olm1.m	$$⊢\underset{\dot{}}{\wedge }=\mathrm{meet}\left(K\right)$$
3		olm1.u	$$⊢\underset{\dot{}}{1}=\mathrm{1.}\left(K\right)$$
4		olop	$$⊢K\in \mathrm{OL}\to K\in \mathrm{OP}$$
5	4	adantr	$$⊢\left(K\in \mathrm{OL}\wedge X\in B\right)\to K\in \mathrm{OP}$$
6		eqid	$$⊢\mathrm{0.}\left(K\right)=\mathrm{0.}\left(K\right)$$
7		eqid	$$⊢\mathrm{oc}\left(K\right)=\mathrm{oc}\left(K\right)$$
8	6 3 7	opoc1	$$⊢K\in \mathrm{OP}\to \mathrm{oc}\left(K\right)\left(\underset{\dot{}}{1}\right)=\mathrm{0.}\left(K\right)$$
9	5 8	syl	$$⊢\left(K\in \mathrm{OL}\wedge X\in B\right)\to \mathrm{oc}\left(K\right)\left(\underset{\dot{}}{1}\right)=\mathrm{0.}\left(K\right)$$
10	9	oveq2d	$$⊢\left(K\in \mathrm{OL}\wedge X\in B\right)\to \mathrm{oc}\left(K\right)\left(X\right)\mathrm{join}\left(K\right)\mathrm{oc}\left(K\right)\left(\underset{\dot{}}{1}\right)=\mathrm{oc}\left(K\right)\left(X\right)\mathrm{join}\left(K\right)\mathrm{0.}\left(K\right)$$
11	1 7	opoccl	$$⊢\left(K\in \mathrm{OP}\wedge X\in B\right)\to \mathrm{oc}\left(K\right)\left(X\right)\in B$$
12	4 11	sylan	$$⊢\left(K\in \mathrm{OL}\wedge X\in B\right)\to \mathrm{oc}\left(K\right)\left(X\right)\in B$$
13		eqid	$$⊢\mathrm{join}\left(K\right)=\mathrm{join}\left(K\right)$$
14	1 13 6	olj01	$$⊢\left(K\in \mathrm{OL}\wedge \mathrm{oc}\left(K\right)\left(X\right)\in B\right)\to \mathrm{oc}\left(K\right)\left(X\right)\mathrm{join}\left(K\right)\mathrm{0.}\left(K\right)=\mathrm{oc}\left(K\right)\left(X\right)$$
15	12 14	syldan	$$⊢\left(K\in \mathrm{OL}\wedge X\in B\right)\to \mathrm{oc}\left(K\right)\left(X\right)\mathrm{join}\left(K\right)\mathrm{0.}\left(K\right)=\mathrm{oc}\left(K\right)\left(X\right)$$
16	10 15	eqtrd	$$⊢\left(K\in \mathrm{OL}\wedge X\in B\right)\to \mathrm{oc}\left(K\right)\left(X\right)\mathrm{join}\left(K\right)\mathrm{oc}\left(K\right)\left(\underset{\dot{}}{1}\right)=\mathrm{oc}\left(K\right)\left(X\right)$$
17	16	fveq2d	$$⊢\left(K\in \mathrm{OL}\wedge X\in B\right)\to \mathrm{oc}\left(K\right)\left(\mathrm{oc}\left(K\right)\left(X\right)\mathrm{join}\left(K\right)\mathrm{oc}\left(K\right)\left(\underset{\dot{}}{1}\right)\right)=\mathrm{oc}\left(K\right)\left(\mathrm{oc}\left(K\right)\left(X\right)\right)$$
18	1 3	op1cl	$$⊢K\in \mathrm{OP}\to \underset{\dot{}}{1}\in B$$
19	5 18	syl	$$⊢\left(K\in \mathrm{OL}\wedge X\in B\right)\to \underset{\dot{}}{1}\in B$$
20	1 13 2 7	oldmj4	$$⊢\left(K\in \mathrm{OL}\wedge X\in B\wedge \underset{\dot{}}{1}\in B\right)\to \mathrm{oc}\left(K\right)\left(\mathrm{oc}\left(K\right)\left(X\right)\mathrm{join}\left(K\right)\mathrm{oc}\left(K\right)\left(\underset{\dot{}}{1}\right)\right)=X\underset{\dot{}}{\wedge }\underset{\dot{}}{1}$$
21	19 20	mpd3an3	$$⊢\left(K\in \mathrm{OL}\wedge X\in B\right)\to \mathrm{oc}\left(K\right)\left(\mathrm{oc}\left(K\right)\left(X\right)\mathrm{join}\left(K\right)\mathrm{oc}\left(K\right)\left(\underset{\dot{}}{1}\right)\right)=X\underset{\dot{}}{\wedge }\underset{\dot{}}{1}$$
22	1 7	opococ	$$⊢\left(K\in \mathrm{OP}\wedge X\in B\right)\to \mathrm{oc}\left(K\right)\left(\mathrm{oc}\left(K\right)\left(X\right)\right)=X$$
23	4 22	sylan	$$⊢\left(K\in \mathrm{OL}\wedge X\in B\right)\to \mathrm{oc}\left(K\right)\left(\mathrm{oc}\left(K\right)\left(X\right)\right)=X$$
24	17 21 23	3eqtr3d	$$⊢\left(K\in \mathrm{OL}\wedge X\in B\right)\to X\underset{\dot{}}{\wedge }\underset{\dot{}}{1}=X$$