HomeHome Metamath Proof Explorer < Previous   Next >
Related theorems
Unicode version
Theorem ecoprass 4304
Description: Lemma used to transfer an associative law via an equivalence relation.
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 groups:   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 3953 . . . 4 |- ([<.x, y>.]R = A -> ([<.x, y>.]RF[<.z, w>.]R) = (AF[<.z, w>.]R))
32opreq1d 3960 . . 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 3953 . . 3 |- ([<.x, y>.]R = A -> ([<.x, y>.]RF([<.z, w>.]RF[<.v, u>.]R)) = (AF([<.z, w>.]RF[<.v, u>.]R)))
53, 4eqeq12d 1481 . 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 3954 . . . 4 |- ([<.z, w>.]R = B -> (AF[<.z, w>.]R) = (AFB))
76opreq1d 3960 . . 3 |- ([<.z, w>.]R = B -> ((AF[<.z, w>.]R)F[<.v, u>.]R) = ((AFB)F[<.v, u>.]R))
8 opreq1 3953 . . . 4 |- ([<.z, w>.]R = B -> ([<.z, w>.]RF[<.v, u>.]R) = (BF[<.v, u>.]R))
98opreq2d 3961 . . 3 |- ([<.z, w>.]R = B -> (AF([<.z, w>.]RF[<.v, u>.]R)) = (AF(BF[<.v, u>.]R)))
107, 9eqeq12d 1481 . 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 3954 . . 3 |- ([<.v, u>.]R = C -> ((AFB)F[<.v, u>.]R) = ((AFB)FC))
12 opreq2 3954 . . . 4 |- ([<.v, u>.]R = C -> (BF[<.v, u>.]R) = (BFC))
1312opreq2d 3961 . . 3 |- ([<.v, u>.]R = C -> (AF(BF[<.v, u>.]R)) = (AF(BFC)))
1411, 13eqeq12d 1481 . 2 |- ([<.v, u>.]R = C -> (((AFB)F[<.v, u>.]R) = (AF(BF[<.v, u>.]R)) <-> ((AFB)FC) = (AF(BFC))))
15 ecoprass.8 . . . 4 |- J = L
16 ecoprass.9 . . . 4 |- K = M
17 opeq12 2480 . . . . 5 |- ((J = L /\ K = M) -> <.J, K>. = <.L, M>.)
18 eceq2 4262 . . . . 5 |- (<.J, K>. = <.L, M>. -> [<.J, K>.]R = [<.L, M>.]R)
1917, 18syl 10 . . . 4 |- ((J = L /\ K = M) -> [<.J, K>.]R = [<.L, M>.]R)
2015, 16, 19mp2an 695 . . 3 |- [<.J, K>.]R = [<.L, M>.]R
21 ecoprass.2 . . . . . . 7 |- (((x e. S /\ y e. S) /\ (z e. S /\ w e. S)) -> ([<.x, y>.]RF[<.z, w>.]R) = [<.G, H>.]R)
2221opreq1d 3960 . . . . . 6 |- (((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))
2322adantr 389 . . . . 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) = ([<.G, H>.]RF[<.v, u>.]R))
24 ecoprass.4 . . . . . 6 |- (((G e. S /\ H e. S) /\ (v e. S /\ u e. S)) -> ([<.G, H>.]RF[<.v, u>.]R) = [<.J, K>.]R)
25 ecoprass.6 . . . . . 6 |- (((x e. S /\ y e. S) /\ (z e. S /\ w e. S)) -> (G e. S /\ H e. S))
2624, 25sylan 448 . . . . 5 |- ((((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)
2723, 26eqtrd 1499 . . . 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)
28273impa 826 . . 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) = [<.J, K>.]R)
29 ecoprass.3 . . . . . . 7 |- (((z e. S /\ w e. S) /\ (v e. S /\ u e. S)) -> ([<.z, w>.]RF[<.v, u>.]R) = [<.N, Q>.]R)
3029opreq2d 3961 . . . . . 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))
3130adantl 388 . . . . 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))
32 ecoprass.5 . . . . . 6 |- (((x e. S /\ y e. S) /\ (N e. S /\ Q e. S)) -> ([<.x, y>.]RF[<.N, Q>.]R) = [<.L, M>.]R)
33 ecoprass.7 . . . . . 6 |- (((z e. S /\ w e. S) /\ (v e. S /\ u e. S)) -> (N e. S /\ Q e. S))
3432, 33sylan2 451 . . . . 5 |- (((x e. S /\ y e. S) /\ ((z e. S /\ w e. S) /\ (v e. S /\ u