HomeHome Metamath Proof Explorer < Previous   Next >
Related theorems
Unicode version
Theorem ecoprass 5190
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 4700 . . . 4 |- ([<.x, y>.]R = A -> ([<.x, y>.]RF[<.z, w>.]R) = (AF[<.z, w>.]R))
32opreq1d 4708 . . 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 4700 . . 3 |- ([<.x, y>.]R = A -> ([<.x, y>.]RF([<.z, w>.]RF[<.v, u>.]R)) = (AF([<.z, w>.]RF[<.v, u>.]R)))
53, 4eqeq12d 1736 . 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 4701 . . . 4 |- ([<.z, w>.]R = B -> (AF[<.z, w>.]R) = (AFB))
76opreq1d 4708 . . 3 |- ([<.z, w>.]R = B -> ((AF[<.z, w>.]R)F[<.v, u>.]R) = ((AFB)F[<.v, u>.]R))
8 opreq1 4700 . . . 4 |- ([<.z, w>.]R = B -> ([<.z, w>.]RF[<.v, u>.]R) = (BF[<.v, u>.]R))
98opreq2d 4709 . . 3 |- ([<.z, w>.]R = B -> (AF([<.z, w>.]RF[<.v, u>.]R)) = (AF(BF[<.v, u>.]R)))
107, 9eqeq12d 1736 . 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 4701 . . 3 |- ([<.v, u>.]R = C -> ((AFB)F[<.v, u>.]R) = ((AFB)FC))
12 opreq2 4701 . . . 4 |- ([<.v, u>.]R = C -> (BF[<.v, u>.]R) = (BFC))
1312opreq2d 4709 . . 3 |- ([<.v, u>.]R = C -> (AF(BF[<.v, u>.]R)) = (AF(BFC)))
1411, 13eqeq12d 1736 . 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 2982 . . . . 5 |- ((J = L /\ K = M) -> <.J, K>. = <.L, M>.)
18 eceq2 5147 . . . . 5 |- (<.J, K>. = <.L, M>. -> [<.J, K>.]R = [<.L, M>.]R)
1917, 18syl 12 . . . 4 |- ((J = L /\ K = M) -> [<.J, K>.]R = [<.L, M>.]R)
2015, 16, 19mp2an 758 . . 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 4708 . . . . . 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 423 . . . . 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 495 . . . . 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 1762 . . . 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 941 . . 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 4709 . . . . . 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 422 . . . . 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 498 . . . . 5 |- (((x e. S /\ y e. S) /\ ((z e. S /\ w e. S) /\ (v e. S /\ u e. S))) -> ([<.x, y>.]RF[<.N, Q>.]R) = [<.L, M>.]R)
3531, 34eqtrd 1762 . . . 4 |- (((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)) = [<.L, M>.]R)
36353impb 942 . . 3 |- (((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)) = [<.L, M>.]R)
3720, 28, 363eqtr4a 1791 . 2 |- (((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) = ([<.x, y>.]RF([<.z, w>.]RF[<.v, u>.]R)))
381, 5, 10, 14, 373ecoptocl 5175 1 |- ((A e. D /\ B e. D /\ C e. D) -> ((AFB)FC) = (AF(BFC)))
Colors of variables: wff set class
Syntax hints:   -> wi 3   /\ wa 239   /\ w3a 855   = wceq 1136   e. wcel 1138  <.cop 2870   X. cxp 3795  (class class class)co 4695  [cec 5127  /.cqs 5128
This theorem is referenced by:  addasspq 6011  mulasspq 6013  addasssr 6145  mulasssr 6147  axaddass 6226  axmulass 6227
This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 1142  ax-gen 1143  ax-8 1144  ax-9 1145  ax-10 1146  ax-11 1147  ax-12 1148  ax-14 1150  ax-17 1155  ax-4 1157  ax-5o 1159  ax-6o 1162  ax-9o 1319  ax-10o 1338  ax-16 1418  ax-11o 1426  ax-ext 1702  ax-sep 3253  ax-nul 3260  ax-pow 3296  ax-pr 3339
This theorem depends on definitions:  df-bi 163  df-or 240  df-an 241  df-3an 857  df-ex 1165  df-sb 1374  df-eu 1613  df-mo 1614  df-clab 1709  df-cleq 1714  df-clel 1717  df-ne 1856  df-ral 1943  df-rex 1944  df-v 2127  df-dif 2430  df-un 2433  df-in 2436  df-ss 2438  df-nul 2702  df-pw 2859  df-sn 2873  df-pr 2874  df-op 2877  df-uni 3000  df-br 3159  df-opab 3214  df-xp 3811  df-cnv 3813  df-dm 3815  df-rn 3816  df-res 3817  df-ima 3818  df-fv 3825  df-opr 4697  df-ec 5131  df-qs 5134
Copyright terms: Public domain