HomeHome Metamath Proof Explorer < Previous   Next >
Related theorems
Unicode version
Theorem ecoprass 3256
Description: Lemma used in proving associative laws via equivalence classes.
Hypotheses
Ref Expression
ecoprass.1 |- D = ((S X. S)/.R)
ecoprass.2 |- (((x e. S /\ y e. S) /\ (z e. S /\ w e. S)) -> ([<.x, y>.]RF[<.z, w>.]R) = [<.G, H>.]R)
ecoprass.3 |- (((z e. S /\ w e. S) /\ (v e. S /\ u e. S)) -> ([<.z, w>.]RF[<.v, u>.]R) = [<.N, Q>.]R)
ecoprass.4 |- (((G e. S /\ H e. S) /\ (v e. S /\ u e. S)) -> ([<.G, H>.]RF[<.v, u>.]R) = [<.J, K>.]R)
ecoprass.5 |- (((x e. S /\ y e. S) /\ (N e. S /\ Q e. S)) -> ([<.x, y>.]RF[<.N, Q>.]R) = [<.L, M>.]R)
ecoprass.6 |- (((x e. S /\ y e. S) /\ (z e. S /\ w e. S)) -> (G e. S /\ H e. S))
ecoprass.7 |- (((z e. S /\ w e. S) /\ (v e. S /\ u e. S)) -> (N e. S /\ Q e. S))
ecoprass.8 |- J = L
ecoprass.9 |- K = M
Assertion
Ref Expression
ecoprass |- ((A e. D /\ B e. D /\ C e. D) -> ((AFB)FC) = (AF(BFC)))
Distinct variable group(s):   x,y,z,w,v,u,A   x,B,y,z,w,v,u   x,C,y,z,w,v,u   x,F,y,z,w,v,u   x,R,y,z,w,v,u   x,S,y,z,w,v,u   z,D,w,v,u
Proof of Theorem ecoprass
StepHypRef Expression
1 ecoprass.1 . 2 |- D = ((S X. S)/.R)
2 opreq1 3006 . . . 4 |- ([<.x, y>.]R = A -> ([<.x, y>.]RF[<.z, w>.]R) = (AF[<.z, w>.]R))
32opreq1d 3012 . . 3 |- ([<.x, y>.]R = A -> (([<.x, y>.]RF[<.z, w>.]R)F[<.v, u>.]R) = ((AF[<.z, w>.]R)F[<.v, u>.]R))
4 opreq1 3006 . . 3 |- ([<.x, y>.]R = A -> ([<.x, y>.]RF([<.z, w>.]RF[<.v, u>.]R)) = (AF([<.z, w>.]RF[<.v, u>.]R)))
53, 4cleq12d 1115 . 2 |- ([<.x, y>.]R = A -> ((([<.x, y>.]RF[<.z, w>.]R)F[<.v, u>.]R) = ([<.x, y>.]RF([<.z, w>.]RF[<.v, u>.]R)) <-> ((AF[<.z, w>.]R)F[<.v, u>.]R) = (AF([<.z, w>.]RF[<.v, u>.]R))))
6 opreq2 3007 . . . 4 |- ([<.z, w>.]R = B -> (AF[<.z, w>.]R) = (AFB))
76opreq1d 3012 . . 3 |- ([<.z, w>.]R = B -> ((AF[<.z, w>.]R)F[<.v, u>.]R) = ((AFB)F[<.v, u>.]R))
8 opreq1 3006 . . . 4 |- ([<.z, w>.]R = B -> ([<.z, w>.]RF[<.v, u>.]R) = (BF[<.v, u>.]R))
98opreq2d 3013 . . 3 |- ([<.z, w>.]R = B -> (AF([<.z, w>.]RF[<.v, u>.]R)) = (AF(BF[<.v, u>.]R)))
107, 9cleq12d 1115 . 2 |- ([<.z, w>.]R = B -> (((AF[<.z, w>.]R)F[<.v, u>.]R) = (AF([<.z, w>.]RF[<.v, u>.]R)) <-> ((AFB)F[<.v, u>.]R) = (AF(BF[<.v, u>.]R))))
11 opreq2 3007 . . 3 |- ([<.v, u>.]R = C -> ((AFB)F[<.v, u>.]R) = ((AFB)FC))
12 opreq2 3007 . . . 4 |- ([<.v, u>.]R = C -> (BF[<.v, u>.]R) = (BFC))
1312opreq2d 3013 . . 3 |- ([<.v, u>.]R = C -> (AF(BF[<.v, u>.]R)) = (AF(BFC)))
1411, 13cleq12d 1115 . 2 |- ([<.v, u>.]R = C -> (((AFB)F[<.v, u>.]R) = (AF(BF[<.v, u>.]R)) <-> ((AFB)FC) = (AF(BFC))))
15 ecoprass.2 . . . . . . . 8 |- (((x e. S /\ y e. S) /\ (z e. S /\ w e. S)) -> ([<.x, y>.]RF[<.z, w>.]R) = [<.G, H>.]R)
1615opreq1d 3012 . . . . . . 7 |- (((x e. S /\ y e. S) /\ (z e. S /\ w e. S)) -> (([<.x, y>.]RF[<.z, w>.]R)F[<.v, u>.]R) = ([<.G, H>.]RF[<.v, u>.]R))
1716adantr 306 . . . . . 6 |- ((((x e. S /\ y e. S) /\ (z e. S /\ w e. S)) /\ (v e. S /\ u e. S)) -> (([<.x, y>.]RF[<.z, w>.]R)F[<.v, u>.]R) = ([<.G, H>.]RF[<.v, u>.]R))
18 ecoprass.4 . . . . . . 7 |- (((G e. S /\ H e. S) /\ (v e. S /\ u e. S)) -> ([<.G, H>.]RF[<.v, u>.]R) = [<.J, K>.]R)
19 ecoprass.6 . . . . . . 7 |- (((x e. S /\ y e. S) /\ (z e. S /\ w e. S)) -> (G e. S /\ H e. S))
2018, 19sylan 343 . . . . . 6 |- ((((x e. S /\ y e. S) /\ (z e. S /\ w e. S)) /\ (v e. S /\ u e. S)) -> ([<.G, H>.]RF[<.v, u>.]R) = [<.J, K>.]R)
2117, 20eqtrd 1128 . . . . 5 |- ((((x e. S /\ y e. S) /\ (z e. S /\ w e. S)) /\ (v e. S /\ u e. S)) -> (([<.x, y>.]RF[<.z, w>.]R)F[<.v, u>.]R) = [<.J, K>.]R)
22213impa 609 . . . 4 |- (((x e. S /\ y e. S) /\ (z e. S /\ w e. S) /\ (v e. S /\ u e. S)) -> (([<.x, y>.]RF[<.z, w>.]R)F[<.v, u>.]R) = [<.J, K>.]R)
23 ecoprass.8 . . . . 5 |- J = L
24 ecoprass.9 . . . . 5 |- K = M
25 opeq12 1878 . . . . . 6 |- ((J = L /\ K = M) -> <.J, K>. = <.L, M>.)
26 eceq2 3215 . . . . . 6 |- (<.J, K>. = <.L, M>. -> [<.J, K>.]R = [<.L, M>.]R)
2725, 26syl 12 . . . . 5 |- ((J = L /\ K = M) -> [<.J, K>.]R = [<.L, M>.]R)
2823, 24, 27mp2an 520 . . . 4 |- [<.J, K>.]R = [<.L, M>.]R
2922, 28syl6eq 1140 . . 3 |- (((x e. S /\ y e. S) /\ (z e. S /\ w e. S) /\ (v e. S /\ u e. S)) -> (([<.x, y>.]RF[<.z, w>.]R)F[<.v, u>.]R) = [<.L, M>.]R)
30 ecoprass.3 . . . . . . 7 |- (((z e. S /\ w e. S) /\ (v e. S /\ u e. S)) -> ([<.z, w>.]RF[<.v, u>.]R) = [<.N, Q>.]R)
3130opreq2d 3013 . . . . . 6 |- (((z e. S /\ w e. S) /\ (v e. S /\ u e. S)) -> ([<.x, y>.]RF([<.z, w>.]RF[<.v, u>.]R)) = ([<.x, y>.]RF[<.N, Q>.]R))
3231adantl 305 . . . . 5 |- (((x e. S /\ y e. S) /\ ((z e. S /\ w e. S) /\ (v e. S /\ u e. S))) -> ([<.x, y>.]RF([<.z, w>.]RF[<.v, u>.]R)) = ([<.x, y>.]RF[<.N, Q>.]R))
33 ecoprass.5 . . . . . 6 |- (((x e. S /\ y e. S) /\ (N e. S /\ Q e. S)) -> ([<.x, y>.]RF[<.N, Q>.]R) = [<.L, M>.]R)
34 ecoprass.7 . . . . . 6 |- (((z e. S /\ w e. S) /\