ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  ring1 Unicode version

Theorem ring1 13049
Description: The (smallest) structure representing a zero ring. (Contributed by AV, 28-Apr-2019.)
Hypothesis
Ref Expression
ring1.m  |-  M  =  { <. ( Base `  ndx ) ,  { Z } >. ,  <. ( +g  `  ndx ) ,  { <. <. Z ,  Z >. ,  Z >. } >. , 
<. ( .r `  ndx ) ,  { <. <. Z ,  Z >. ,  Z >. }
>. }
Assertion
Ref Expression
ring1  |-  ( Z  e.  V  ->  M  e.  Ring )

Proof of Theorem ring1
Dummy variables  a  b  c  x  y are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 snexg 4181 . . . . . . . 8  |-  ( Z  e.  V  ->  { Z }  e.  _V )
2 opexg 4224 . . . . . . . . . . 11  |-  ( ( Z  e.  V  /\  Z  e.  V )  -> 
<. Z ,  Z >.  e. 
_V )
32anidms 397 . . . . . . . . . 10  |-  ( Z  e.  V  ->  <. Z ,  Z >.  e.  _V )
4 opexg 4224 . . . . . . . . . 10  |-  ( (
<. Z ,  Z >.  e. 
_V  /\  Z  e.  V )  ->  <. <. Z ,  Z >. ,  Z >.  e. 
_V )
53, 4mpancom 422 . . . . . . . . 9  |-  ( Z  e.  V  ->  <. <. Z ,  Z >. ,  Z >.  e. 
_V )
6 snexg 4181 . . . . . . . . 9  |-  ( <. <. Z ,  Z >. ,  Z >.  e.  _V  ->  { <. <. Z ,  Z >. ,  Z >. }  e.  _V )
75, 6syl 14 . . . . . . . 8  |-  ( Z  e.  V  ->  { <. <. Z ,  Z >. ,  Z >. }  e.  _V )
8 ring1.m . . . . . . . . 9  |-  M  =  { <. ( Base `  ndx ) ,  { Z } >. ,  <. ( +g  `  ndx ) ,  { <. <. Z ,  Z >. ,  Z >. } >. , 
<. ( .r `  ndx ) ,  { <. <. Z ,  Z >. ,  Z >. }
>. }
98rngbaseg 12560 . . . . . . . 8  |-  ( ( { Z }  e.  _V  /\  { <. <. Z ,  Z >. ,  Z >. }  e.  _V  /\  { <. <. Z ,  Z >. ,  Z >. }  e.  _V )  ->  { Z }  =  ( Base `  M ) )
101, 7, 7, 9syl3anc 1238 . . . . . . 7  |-  ( Z  e.  V  ->  { Z }  =  ( Base `  M ) )
1110opeq2d 3783 . . . . . 6  |-  ( Z  e.  V  ->  <. ( Base `  ndx ) ,  { Z } >.  = 
<. ( Base `  ndx ) ,  ( Base `  M ) >. )
128rngplusgg 12561 . . . . . . . 8  |-  ( ( { Z }  e.  _V  /\  { <. <. Z ,  Z >. ,  Z >. }  e.  _V  /\  { <. <. Z ,  Z >. ,  Z >. }  e.  _V )  ->  { <. <. Z ,  Z >. ,  Z >. }  =  ( +g  `  M ) )
131, 7, 7, 12syl3anc 1238 . . . . . . 7  |-  ( Z  e.  V  ->  { <. <. Z ,  Z >. ,  Z >. }  =  ( +g  `  M ) )
1413opeq2d 3783 . . . . . 6  |-  ( Z  e.  V  ->  <. ( +g  `  ndx ) ,  { <. <. Z ,  Z >. ,  Z >. } >.  = 
<. ( +g  `  ndx ) ,  ( +g  `  M ) >. )
1511, 14preq12d 3676 . . . . 5  |-  ( Z  e.  V  ->  { <. (
Base `  ndx ) ,  { Z } >. , 
<. ( +g  `  ndx ) ,  { <. <. Z ,  Z >. ,  Z >. }
>. }  =  { <. (
Base `  ndx ) ,  ( Base `  M
) >. ,  <. ( +g  `  ndx ) ,  ( +g  `  M
) >. } )
16 eqid 2177 . . . . . 6  |-  { <. (
Base `  ndx ) ,  { Z } >. , 
<. ( +g  `  ndx ) ,  { <. <. Z ,  Z >. ,  Z >. }
>. }  =  { <. (
Base `  ndx ) ,  { Z } >. , 
<. ( +g  `  ndx ) ,  { <. <. Z ,  Z >. ,  Z >. }
>. }
1716grp1 12852 . . . . 5  |-  ( Z  e.  V  ->  { <. (
Base `  ndx ) ,  { Z } >. , 
<. ( +g  `  ndx ) ,  { <. <. Z ,  Z >. ,  Z >. }
>. }  e.  Grp )
1815, 17eqeltrrd 2255 . . . 4  |-  ( Z  e.  V  ->  { <. (
Base `  ndx ) ,  ( Base `  M
) >. ,  <. ( +g  `  ndx ) ,  ( +g  `  M
) >. }  e.  Grp )
19 basendxnn 12487 . . . . . . . 8  |-  ( Base `  ndx )  e.  NN
20 opexg 4224 . . . . . . . 8  |-  ( ( ( Base `  ndx )  e.  NN  /\  { Z }  e.  _V )  ->  <. ( Base `  ndx ) ,  { Z } >.  e.  _V )
2119, 1, 20sylancr 414 . . . . . . 7  |-  ( Z  e.  V  ->  <. ( Base `  ndx ) ,  { Z } >.  e. 
_V )
22 plusgslid 12538 . . . . . . . . 9  |-  ( +g  = Slot  ( +g  `  ndx )  /\  ( +g  `  ndx )  e.  NN )
2322simpri 113 . . . . . . . 8  |-  ( +g  ` 
ndx )  e.  NN
24 opexg 4224 . . . . . . . 8  |-  ( ( ( +g  `  ndx )  e.  NN  /\  { <. <. Z ,  Z >. ,  Z >. }  e.  _V )  ->  <. ( +g  `  ndx ) ,  { <. <. Z ,  Z >. ,  Z >. } >.  e. 
_V )
2523, 7, 24sylancr 414 . . . . . . 7  |-  ( Z  e.  V  ->  <. ( +g  `  ndx ) ,  { <. <. Z ,  Z >. ,  Z >. } >.  e. 
_V )
26 mulrslid 12556 . . . . . . . . 9  |-  ( .r  = Slot  ( .r `  ndx )  /\  ( .r `  ndx )  e.  NN )
2726simpri 113 . . . . . . . 8  |-  ( .r
`  ndx )  e.  NN
28 opexg 4224 . . . . . . . 8  |-  ( ( ( .r `  ndx )  e.  NN  /\  { <. <. Z ,  Z >. ,  Z >. }  e.  _V )  ->  <. ( .r `  ndx ) ,  { <. <. Z ,  Z >. ,  Z >. } >.  e. 
_V )
2927, 7, 28sylancr 414 . . . . . . 7  |-  ( Z  e.  V  ->  <. ( .r `  ndx ) ,  { <. <. Z ,  Z >. ,  Z >. } >.  e. 
_V )
30 tpexg 4440 . . . . . . 7  |-  ( (
<. ( Base `  ndx ) ,  { Z } >.  e.  _V  /\  <.
( +g  `  ndx ) ,  { <. <. Z ,  Z >. ,  Z >. } >.  e. 
_V  /\  <. ( .r
`  ndx ) ,  { <. <. Z ,  Z >. ,  Z >. } >.  e. 
_V )  ->  { <. (
Base `  ndx ) ,  { Z } >. , 
<. ( +g  `  ndx ) ,  { <. <. Z ,  Z >. ,  Z >. }
>. ,  <. ( .r
`  ndx ) ,  { <. <. Z ,  Z >. ,  Z >. } >. }  e.  _V )
3121, 25, 29, 30syl3anc 1238 . . . . . 6  |-  ( Z  e.  V  ->  { <. (
Base `  ndx ) ,  { Z } >. , 
<. ( +g  `  ndx ) ,  { <. <. Z ,  Z >. ,  Z >. }
>. ,  <. ( .r
`  ndx ) ,  { <. <. Z ,  Z >. ,  Z >. } >. }  e.  _V )
328, 31eqeltrid 2264 . . . . 5  |-  ( Z  e.  V  ->  M  e.  _V )
33 eqid 2177 . . . . . 6  |-  ( Base `  M )  =  (
Base `  M )
34 eqid 2177 . . . . . 6  |-  ( +g  `  M )  =  ( +g  `  M )
35 eqid 2177 . . . . . 6  |-  { <. (
Base `  ndx ) ,  ( Base `  M
) >. ,  <. ( +g  `  ndx ) ,  ( +g  `  M
) >. }  =  { <. ( Base `  ndx ) ,  ( Base `  M ) >. ,  <. ( +g  `  ndx ) ,  ( +g  `  M
) >. }
3633, 34, 35grppropstrg 12772 . . . . 5  |-  ( M  e.  _V  ->  ( M  e.  Grp  <->  { <. ( Base `  ndx ) ,  ( Base `  M
) >. ,  <. ( +g  `  ndx ) ,  ( +g  `  M
) >. }  e.  Grp ) )
3732, 36syl 14 . . . 4  |-  ( Z  e.  V  ->  ( M  e.  Grp  <->  { <. ( Base `  ndx ) ,  ( Base `  M
) >. ,  <. ( +g  `  ndx ) ,  ( +g  `  M
) >. }  e.  Grp ) )
3818, 37mpbird 167 . . 3  |-  ( Z  e.  V  ->  M  e.  Grp )
3916mnd1 12724 . . . 4  |-  ( Z  e.  V  ->  { <. (
Base `  ndx ) ,  { Z } >. , 
<. ( +g  `  ndx ) ,  { <. <. Z ,  Z >. ,  Z >. }
>. }  e.  Mnd )
40 eqidd 2178 . . . . 5  |-  ( Z  e.  V  ->  ( Base `  (mulGrp `  M
) )  =  (
Base `  (mulGrp `  M
) ) )
4116grpbaseg 12551 . . . . . . 7  |-  ( ( { Z }  e.  _V  /\  { <. <. Z ,  Z >. ,  Z >. }  e.  _V )  ->  { Z }  =  (
Base `  { <. ( Base `  ndx ) ,  { Z } >. , 
<. ( +g  `  ndx ) ,  { <. <. Z ,  Z >. ,  Z >. }
>. } ) )
421, 7, 41syl2anc 411 . . . . . 6  |-  ( Z  e.  V  ->  { Z }  =  ( Base `  { <. ( Base `  ndx ) ,  { Z } >. ,  <. ( +g  `  ndx ) ,  { <. <. Z ,  Z >. ,  Z >. } >. } ) )
43 eqid 2177 . . . . . . . 8  |-  (mulGrp `  M )  =  (mulGrp `  M )
4443, 33mgpbasg 12950 . . . . . . 7  |-  ( M  e.  _V  ->  ( Base `  M )  =  ( Base `  (mulGrp `  M ) ) )
4532, 44syl 14 . . . . . 6  |-  ( Z  e.  V  ->  ( Base `  M )  =  ( Base `  (mulGrp `  M ) ) )
4610, 42, 453eqtr3rd 2219 . . . . 5  |-  ( Z  e.  V  ->  ( Base `  (mulGrp `  M
) )  =  (
Base `  { <. ( Base `  ndx ) ,  { Z } >. , 
<. ( +g  `  ndx ) ,  { <. <. Z ,  Z >. ,  Z >. }
>. } ) )
478rngmulrg 12562 . . . . . . . 8  |-  ( ( { Z }  e.  _V  /\  { <. <. Z ,  Z >. ,  Z >. }  e.  _V  /\  { <. <. Z ,  Z >. ,  Z >. }  e.  _V )  ->  { <. <. Z ,  Z >. ,  Z >. }  =  ( .r `  M ) )
481, 7, 7, 47syl3anc 1238 . . . . . . 7  |-  ( Z  e.  V  ->  { <. <. Z ,  Z >. ,  Z >. }  =  ( .r `  M ) )
4916grpplusgg 12552 . . . . . . . 8  |-  ( ( { Z }  e.  _V  /\  { <. <. Z ,  Z >. ,  Z >. }  e.  _V )  ->  { <. <. Z ,  Z >. ,  Z >. }  =  ( +g  `  { <. (
Base `  ndx ) ,  { Z } >. , 
<. ( +g  `  ndx ) ,  { <. <. Z ,  Z >. ,  Z >. }
>. } ) )
501, 7, 49syl2anc 411 . . . . . . 7  |-  ( Z  e.  V  ->  { <. <. Z ,  Z >. ,  Z >. }  =  ( +g  `  { <. (
Base `  ndx ) ,  { Z } >. , 
<. ( +g  `  ndx ) ,  { <. <. Z ,  Z >. ,  Z >. }
>. } ) )
51 eqid 2177 . . . . . . . . 9  |-  ( .r
`  M )  =  ( .r `  M
)
5243, 51mgpplusgg 12948 . . . . . . . 8  |-  ( M  e.  _V  ->  ( .r `  M )  =  ( +g  `  (mulGrp `  M ) ) )
5332, 52syl 14 . . . . . . 7  |-  ( Z  e.  V  ->  ( .r `  M )  =  ( +g  `  (mulGrp `  M ) ) )
5448, 50, 533eqtr3rd 2219 . . . . . 6  |-  ( Z  e.  V  ->  ( +g  `  (mulGrp `  M
) )  =  ( +g  `  { <. (
Base `  ndx ) ,  { Z } >. , 
<. ( +g  `  ndx ) ,  { <. <. Z ,  Z >. ,  Z >. }
>. } ) )
5554oveqdr 5896 . . . . 5  |-  ( ( Z  e.  V  /\  ( x  e.  ( Base `  (mulGrp `  M
) )  /\  y  e.  ( Base `  (mulGrp `  M ) ) ) )  ->  ( x
( +g  `  (mulGrp `  M ) ) y )  =  ( x ( +g  `  { <. ( Base `  ndx ) ,  { Z } >. ,  <. ( +g  `  ndx ) ,  { <. <. Z ,  Z >. ,  Z >. } >. } ) y ) )
5640, 46, 55mndpropd 12720 . . . 4  |-  ( Z  e.  V  ->  (
(mulGrp `  M )  e.  Mnd  <->  { <. ( Base `  ndx ) ,  { Z } >. ,  <. ( +g  `  ndx ) ,  { <. <. Z ,  Z >. ,  Z >. } >. }  e.  Mnd ) )
5739, 56mpbird 167 . . 3  |-  ( Z  e.  V  ->  (mulGrp `  M )  e.  Mnd )
58 df-ov 5871 . . . . . . 7  |-  ( Z { <. <. Z ,  Z >. ,  Z >. } Z
)  =  ( {
<. <. Z ,  Z >. ,  Z >. } `  <. Z ,  Z >. )
59 fvsng 5707 . . . . . . . 8  |-  ( (
<. Z ,  Z >.  e. 
_V  /\  Z  e.  V )  ->  ( { <. <. Z ,  Z >. ,  Z >. } `  <. Z ,  Z >. )  =  Z )
603, 59mpancom 422 . . . . . . 7  |-  ( Z  e.  V  ->  ( { <. <. Z ,  Z >. ,  Z >. } `  <. Z ,  Z >. )  =  Z )
6158, 60eqtrid 2222 . . . . . 6  |-  ( Z  e.  V  ->  ( Z { <. <. Z ,  Z >. ,  Z >. } Z
)  =  Z )
6261oveq2d 5884 . . . . 5  |-  ( Z  e.  V  ->  ( Z { <. <. Z ,  Z >. ,  Z >. }  ( Z { <. <. Z ,  Z >. ,  Z >. } Z
) )  =  ( Z { <. <. Z ,  Z >. ,  Z >. } Z ) )
6361, 61oveq12d 5886 . . . . 5  |-  ( Z  e.  V  ->  (
( Z { <. <. Z ,  Z >. ,  Z >. } Z ) { <. <. Z ,  Z >. ,  Z >. }  ( Z { <. <. Z ,  Z >. ,  Z >. } Z
) )  =  ( Z { <. <. Z ,  Z >. ,  Z >. } Z ) )
6462, 63eqtr4d 2213 . . . 4  |-  ( Z  e.  V  ->  ( Z { <. <. Z ,  Z >. ,  Z >. }  ( Z { <. <. Z ,  Z >. ,  Z >. } Z
) )  =  ( ( Z { <. <. Z ,  Z >. ,  Z >. } Z ) { <. <. Z ,  Z >. ,  Z >. }  ( Z { <. <. Z ,  Z >. ,  Z >. } Z
) ) )
6561oveq1d 5883 . . . . 5  |-  ( Z  e.  V  ->  (
( Z { <. <. Z ,  Z >. ,  Z >. } Z ) { <. <. Z ,  Z >. ,  Z >. } Z
)  =  ( Z { <. <. Z ,  Z >. ,  Z >. } Z
) )
6665, 63eqtr4d 2213 . . . 4  |-  ( Z  e.  V  ->  (
( Z { <. <. Z ,  Z >. ,  Z >. } Z ) { <. <. Z ,  Z >. ,  Z >. } Z
)  =  ( ( Z { <. <. Z ,  Z >. ,  Z >. } Z ) { <. <. Z ,  Z >. ,  Z >. }  ( Z { <. <. Z ,  Z >. ,  Z >. } Z
) ) )
67 oveq1 5875 . . . . . . . . 9  |-  ( a  =  Z  ->  (
a { <. <. Z ,  Z >. ,  Z >. }  ( b { <. <. Z ,  Z >. ,  Z >. } c ) )  =  ( Z { <. <. Z ,  Z >. ,  Z >. }  (
b { <. <. Z ,  Z >. ,  Z >. } c ) ) )
68 oveq1 5875 . . . . . . . . . 10  |-  ( a  =  Z  ->  (
a { <. <. Z ,  Z >. ,  Z >. } b )  =  ( Z { <. <. Z ,  Z >. ,  Z >. } b ) )
69 oveq1 5875 . . . . . . . . . 10  |-  ( a  =  Z  ->  (
a { <. <. Z ,  Z >. ,  Z >. } c )  =  ( Z { <. <. Z ,  Z >. ,  Z >. } c ) )
7068, 69oveq12d 5886 . . . . . . . . 9  |-  ( a  =  Z  ->  (
( a { <. <. Z ,  Z >. ,  Z >. } b ) { <. <. Z ,  Z >. ,  Z >. }  (
a { <. <. Z ,  Z >. ,  Z >. } c ) )  =  ( ( Z { <. <. Z ,  Z >. ,  Z >. } b ) { <. <. Z ,  Z >. ,  Z >. }  ( Z { <. <. Z ,  Z >. ,  Z >. } c ) ) )
7167, 70eqeq12d 2192 . . . . . . . 8  |-  ( a  =  Z  ->  (
( a { <. <. Z ,  Z >. ,  Z >. }  ( b { <. <. Z ,  Z >. ,  Z >. } c ) )  =  ( ( a { <. <. Z ,  Z >. ,  Z >. } b ) { <. <. Z ,  Z >. ,  Z >. }  (
a { <. <. Z ,  Z >. ,  Z >. } c ) )  <->  ( Z { <. <. Z ,  Z >. ,  Z >. }  (
b { <. <. Z ,  Z >. ,  Z >. } c ) )  =  ( ( Z { <. <. Z ,  Z >. ,  Z >. } b ) { <. <. Z ,  Z >. ,  Z >. }  ( Z { <. <. Z ,  Z >. ,  Z >. } c ) ) ) )
7268oveq1d 5883 . . . . . . . . 9  |-  ( a  =  Z  ->  (
( a { <. <. Z ,  Z >. ,  Z >. } b ) { <. <. Z ,  Z >. ,  Z >. } c )  =  ( ( Z { <. <. Z ,  Z >. ,  Z >. } b ) { <. <. Z ,  Z >. ,  Z >. } c ) )
7369oveq1d 5883 . . . . . . . . 9  |-  ( a  =  Z  ->  (
( a { <. <. Z ,  Z >. ,  Z >. } c ) { <. <. Z ,  Z >. ,  Z >. }  (
b { <. <. Z ,  Z >. ,  Z >. } c ) )  =  ( ( Z { <. <. Z ,  Z >. ,  Z >. } c ) { <. <. Z ,  Z >. ,  Z >. }  ( b { <. <. Z ,  Z >. ,  Z >. } c ) ) )
7472, 73eqeq12d 2192 . . . . . . . 8  |-  ( a  =  Z  ->  (
( ( a {
<. <. Z ,  Z >. ,  Z >. } b ) { <. <. Z ,  Z >. ,  Z >. } c )  =  ( ( a { <. <. Z ,  Z >. ,  Z >. } c ) { <. <. Z ,  Z >. ,  Z >. }  (
b { <. <. Z ,  Z >. ,  Z >. } c ) )  <->  ( ( Z { <. <. Z ,  Z >. ,  Z >. } b ) { <. <. Z ,  Z >. ,  Z >. } c )  =  ( ( Z { <. <. Z ,  Z >. ,  Z >. } c ) { <. <. Z ,  Z >. ,  Z >. }  (
b { <. <. Z ,  Z >. ,  Z >. } c ) ) ) )
7571, 74anbi12d 473 . . . . . . 7  |-  ( a  =  Z  ->  (
( ( a {
<. <. Z ,  Z >. ,  Z >. }  (
b { <. <. Z ,  Z >. ,  Z >. } c ) )  =  ( ( a {
<. <. Z ,  Z >. ,  Z >. } b ) { <. <. Z ,  Z >. ,  Z >. }  ( a { <. <. Z ,  Z >. ,  Z >. } c ) )  /\  ( ( a { <. <. Z ,  Z >. ,  Z >. } b ) { <. <. Z ,  Z >. ,  Z >. } c )  =  ( ( a { <. <. Z ,  Z >. ,  Z >. } c ) { <. <. Z ,  Z >. ,  Z >. }  ( b { <. <. Z ,  Z >. ,  Z >. } c ) ) )  <->  ( ( Z { <. <. Z ,  Z >. ,  Z >. }  (
b { <. <. Z ,  Z >. ,  Z >. } c ) )  =  ( ( Z { <. <. Z ,  Z >. ,  Z >. } b ) { <. <. Z ,  Z >. ,  Z >. }  ( Z { <. <. Z ,  Z >. ,  Z >. } c ) )  /\  ( ( Z { <. <. Z ,  Z >. ,  Z >. } b ) { <. <. Z ,  Z >. ,  Z >. } c )  =  ( ( Z { <. <. Z ,  Z >. ,  Z >. } c ) { <. <. Z ,  Z >. ,  Z >. }  ( b { <. <. Z ,  Z >. ,  Z >. } c ) ) ) ) )
76752ralbidv 2501 . . . . . 6  |-  ( a  =  Z  ->  ( A. b  e.  { Z } A. c  e.  { Z }  ( (
a { <. <. Z ,  Z >. ,  Z >. }  ( b { <. <. Z ,  Z >. ,  Z >. } c ) )  =  ( ( a { <. <. Z ,  Z >. ,  Z >. } b ) { <. <. Z ,  Z >. ,  Z >. }  ( a { <. <. Z ,  Z >. ,  Z >. } c ) )  /\  (
( a { <. <. Z ,  Z >. ,  Z >. } b ) { <. <. Z ,  Z >. ,  Z >. } c )  =  ( ( a { <. <. Z ,  Z >. ,  Z >. } c ) { <. <. Z ,  Z >. ,  Z >. }  ( b { <. <. Z ,  Z >. ,  Z >. } c ) ) )  <->  A. b  e.  { Z } A. c  e.  { Z }  ( ( Z { <. <. Z ,  Z >. ,  Z >. }  (
b { <. <. Z ,  Z >. ,  Z >. } c ) )  =  ( ( Z { <. <. Z ,  Z >. ,  Z >. } b ) { <. <. Z ,  Z >. ,  Z >. }  ( Z { <. <. Z ,  Z >. ,  Z >. } c ) )  /\  ( ( Z { <. <. Z ,  Z >. ,  Z >. } b ) { <. <. Z ,  Z >. ,  Z >. } c )  =  ( ( Z { <. <. Z ,  Z >. ,  Z >. } c ) { <. <. Z ,  Z >. ,  Z >. }  ( b { <. <. Z ,  Z >. ,  Z >. } c ) ) ) ) )
7776ralsng 3631 . . . . 5  |-  ( Z  e.  V  ->  ( A. a  e.  { Z } A. b  e.  { Z } A. c  e. 
{ Z }  (
( a { <. <. Z ,  Z >. ,  Z >. }  ( b { <. <. Z ,  Z >. ,  Z >. } c ) )  =  ( ( a { <. <. Z ,  Z >. ,  Z >. } b ) { <. <. Z ,  Z >. ,  Z >. }  (
a { <. <. Z ,  Z >. ,  Z >. } c ) )  /\  ( ( a {
<. <. Z ,  Z >. ,  Z >. } b ) { <. <. Z ,  Z >. ,  Z >. } c )  =  ( ( a { <. <. Z ,  Z >. ,  Z >. } c ) { <. <. Z ,  Z >. ,  Z >. }  (
b { <. <. Z ,  Z >. ,  Z >. } c ) ) )  <->  A. b  e.  { Z } A. c  e.  { Z }  ( ( Z { <. <. Z ,  Z >. ,  Z >. }  (
b { <. <. Z ,  Z >. ,  Z >. } c ) )  =  ( ( Z { <. <. Z ,  Z >. ,  Z >. } b ) { <. <. Z ,  Z >. ,  Z >. }  ( Z { <. <. Z ,  Z >. ,  Z >. } c ) )  /\  ( ( Z { <. <. Z ,  Z >. ,  Z >. } b ) { <. <. Z ,  Z >. ,  Z >. } c )  =  ( ( Z { <. <. Z ,  Z >. ,  Z >. } c ) { <. <. Z ,  Z >. ,  Z >. }  ( b { <. <. Z ,  Z >. ,  Z >. } c ) ) ) ) )
78 oveq1 5875 . . . . . . . . . 10  |-  ( b  =  Z  ->  (
b { <. <. Z ,  Z >. ,  Z >. } c )  =  ( Z { <. <. Z ,  Z >. ,  Z >. } c ) )
7978oveq2d 5884 . . . . . . . . 9  |-  ( b  =  Z  ->  ( Z { <. <. Z ,  Z >. ,  Z >. }  (
b { <. <. Z ,  Z >. ,  Z >. } c ) )  =  ( Z { <. <. Z ,  Z >. ,  Z >. }  ( Z { <. <. Z ,  Z >. ,  Z >. } c ) ) )
80 oveq2 5876 . . . . . . . . . 10  |-  ( b  =  Z  ->  ( Z { <. <. Z ,  Z >. ,  Z >. } b )  =  ( Z { <. <. Z ,  Z >. ,  Z >. } Z
) )
8180oveq1d 5883 . . . . . . . . 9  |-  ( b  =  Z  ->  (
( Z { <. <. Z ,  Z >. ,  Z >. } b ) { <. <. Z ,  Z >. ,  Z >. }  ( Z { <. <. Z ,  Z >. ,  Z >. } c ) )  =  ( ( Z { <. <. Z ,  Z >. ,  Z >. } Z ) { <. <. Z ,  Z >. ,  Z >. }  ( Z { <. <. Z ,  Z >. ,  Z >. } c ) ) )
8279, 81eqeq12d 2192 . . . . . . . 8  |-  ( b  =  Z  ->  (
( Z { <. <. Z ,  Z >. ,  Z >. }  ( b { <. <. Z ,  Z >. ,  Z >. } c ) )  =  ( ( Z { <. <. Z ,  Z >. ,  Z >. } b ) { <. <. Z ,  Z >. ,  Z >. }  ( Z { <. <. Z ,  Z >. ,  Z >. } c ) )  <->  ( Z { <. <. Z ,  Z >. ,  Z >. }  ( Z { <. <. Z ,  Z >. ,  Z >. } c ) )  =  ( ( Z { <. <. Z ,  Z >. ,  Z >. } Z ) { <. <. Z ,  Z >. ,  Z >. }  ( Z { <. <. Z ,  Z >. ,  Z >. } c ) ) ) )
8380oveq1d 5883 . . . . . . . . 9  |-  ( b  =  Z  ->  (
( Z { <. <. Z ,  Z >. ,  Z >. } b ) { <. <. Z ,  Z >. ,  Z >. } c )  =  ( ( Z { <. <. Z ,  Z >. ,  Z >. } Z ) { <. <. Z ,  Z >. ,  Z >. } c ) )
8478oveq2d 5884 . . . . . . . . 9  |-  ( b  =  Z  ->  (
( Z { <. <. Z ,  Z >. ,  Z >. } c ) { <. <. Z ,  Z >. ,  Z >. }  (
b { <. <. Z ,  Z >. ,  Z >. } c ) )  =  ( ( Z { <. <. Z ,  Z >. ,  Z >. } c ) { <. <. Z ,  Z >. ,  Z >. }  ( Z { <. <. Z ,  Z >. ,  Z >. } c ) ) )
8583, 84eqeq12d 2192 . . . . . . . 8  |-  ( b  =  Z  ->  (
( ( Z { <. <. Z ,  Z >. ,  Z >. } b ) { <. <. Z ,  Z >. ,  Z >. } c )  =  ( ( Z { <. <. Z ,  Z >. ,  Z >. } c ) { <. <. Z ,  Z >. ,  Z >. }  (
b { <. <. Z ,  Z >. ,  Z >. } c ) )  <->  ( ( Z { <. <. Z ,  Z >. ,  Z >. } Z
) { <. <. Z ,  Z >. ,  Z >. } c )  =  ( ( Z { <. <. Z ,  Z >. ,  Z >. } c ) { <. <. Z ,  Z >. ,  Z >. }  ( Z { <. <. Z ,  Z >. ,  Z >. } c ) ) ) )
8682, 85anbi12d 473 . . . . . . 7  |-  ( b  =  Z  ->  (
( ( Z { <. <. Z ,  Z >. ,  Z >. }  (
b { <. <. Z ,  Z >. ,  Z >. } c ) )  =  ( ( Z { <. <. Z ,  Z >. ,  Z >. } b ) { <. <. Z ,  Z >. ,  Z >. }  ( Z { <. <. Z ,  Z >. ,  Z >. } c ) )  /\  ( ( Z { <. <. Z ,  Z >. ,  Z >. } b ) { <. <. Z ,  Z >. ,  Z >. } c )  =  ( ( Z { <. <. Z ,  Z >. ,  Z >. } c ) { <. <. Z ,  Z >. ,  Z >. }  ( b { <. <. Z ,  Z >. ,  Z >. } c ) ) )  <->  ( ( Z { <. <. Z ,  Z >. ,  Z >. }  ( Z { <. <. Z ,  Z >. ,  Z >. } c ) )  =  ( ( Z { <. <. Z ,  Z >. ,  Z >. } Z ) { <. <. Z ,  Z >. ,  Z >. }  ( Z { <. <. Z ,  Z >. ,  Z >. } c ) )  /\  (
( Z { <. <. Z ,  Z >. ,  Z >. } Z ) { <. <. Z ,  Z >. ,  Z >. } c )  =  ( ( Z { <. <. Z ,  Z >. ,  Z >. } c ) { <. <. Z ,  Z >. ,  Z >. }  ( Z { <. <. Z ,  Z >. ,  Z >. } c ) ) ) ) )
8786ralbidv 2477 . . . . . 6  |-  ( b  =  Z  ->  ( A. c  e.  { Z }  ( ( Z { <. <. Z ,  Z >. ,  Z >. }  (
b { <. <. Z ,  Z >. ,  Z >. } c ) )  =  ( ( Z { <. <. Z ,  Z >. ,  Z >. } b ) { <. <. Z ,  Z >. ,  Z >. }  ( Z { <. <. Z ,  Z >. ,  Z >. } c ) )  /\  ( ( Z { <. <. Z ,  Z >. ,  Z >. } b ) { <. <. Z ,  Z >. ,  Z >. } c )  =  ( ( Z { <. <. Z ,  Z >. ,  Z >. } c ) { <. <. Z ,  Z >. ,  Z >. }  ( b { <. <. Z ,  Z >. ,  Z >. } c ) ) )  <->  A. c  e.  { Z }  (
( Z { <. <. Z ,  Z >. ,  Z >. }  ( Z { <. <. Z ,  Z >. ,  Z >. } c ) )  =  ( ( Z { <. <. Z ,  Z >. ,  Z >. } Z ) { <. <. Z ,  Z >. ,  Z >. }  ( Z { <. <. Z ,  Z >. ,  Z >. } c ) )  /\  (
( Z { <. <. Z ,  Z >. ,  Z >. } Z ) { <. <. Z ,  Z >. ,  Z >. } c )  =  ( ( Z { <. <. Z ,  Z >. ,  Z >. } c ) { <. <. Z ,  Z >. ,  Z >. }  ( Z { <. <. Z ,  Z >. ,  Z >. } c ) ) ) ) )
8887ralsng 3631 . . . . 5  |-  ( Z  e.  V  ->  ( A. b  e.  { Z } A. c  e.  { Z }  ( ( Z { <. <. Z ,  Z >. ,  Z >. }  (
b { <. <. Z ,  Z >. ,  Z >. } c ) )  =  ( ( Z { <. <. Z ,  Z >. ,  Z >. } b ) { <. <. Z ,  Z >. ,  Z >. }  ( Z { <. <. Z ,  Z >. ,  Z >. } c ) )  /\  ( ( Z { <. <. Z ,  Z >. ,  Z >. } b ) { <. <. Z ,  Z >. ,  Z >. } c )  =  ( ( Z { <. <. Z ,  Z >. ,  Z >. } c ) { <. <. Z ,  Z >. ,  Z >. }  ( b { <. <. Z ,  Z >. ,  Z >. } c ) ) )  <->  A. c  e.  { Z }  (
( Z { <. <. Z ,  Z >. ,  Z >. }  ( Z { <. <. Z ,  Z >. ,  Z >. } c ) )  =  ( ( Z { <. <. Z ,  Z >. ,  Z >. } Z ) { <. <. Z ,  Z >. ,  Z >. }  ( Z { <. <. Z ,  Z >. ,  Z >. } c ) )  /\  (
( Z { <. <. Z ,  Z >. ,  Z >. } Z ) { <. <. Z ,  Z >. ,  Z >. } c )  =  ( ( Z { <. <. Z ,  Z >. ,  Z >. } c ) { <. <. Z ,  Z >. ,  Z >. }  ( Z { <. <. Z ,  Z >. ,  Z >. } c ) ) ) ) )
89 oveq2 5876 . . . . . . . . 9  |-  ( c  =  Z  ->  ( Z { <. <. Z ,  Z >. ,  Z >. } c )  =  ( Z { <. <. Z ,  Z >. ,  Z >. } Z
) )
9089oveq2d 5884 . . . . . . . 8  |-  ( c  =  Z  ->  ( Z { <. <. Z ,  Z >. ,  Z >. }  ( Z { <. <. Z ,  Z >. ,  Z >. } c ) )  =  ( Z { <. <. Z ,  Z >. ,  Z >. }  ( Z { <. <. Z ,  Z >. ,  Z >. } Z ) ) )
9189oveq2d 5884 . . . . . . . 8  |-  ( c  =  Z  ->  (
( Z { <. <. Z ,  Z >. ,  Z >. } Z ) { <. <. Z ,  Z >. ,  Z >. }  ( Z { <. <. Z ,  Z >. ,  Z >. } c ) )  =  ( ( Z { <. <. Z ,  Z >. ,  Z >. } Z ) { <. <. Z ,  Z >. ,  Z >. }  ( Z { <. <. Z ,  Z >. ,  Z >. } Z
) ) )
9290, 91eqeq12d 2192 . . . . . . 7  |-  ( c  =  Z  ->  (
( Z { <. <. Z ,  Z >. ,  Z >. }  ( Z { <. <. Z ,  Z >. ,  Z >. } c ) )  =  ( ( Z { <. <. Z ,  Z >. ,  Z >. } Z ) { <. <. Z ,  Z >. ,  Z >. }  ( Z { <. <. Z ,  Z >. ,  Z >. } c ) )  <->  ( Z { <. <. Z ,  Z >. ,  Z >. }  ( Z { <. <. Z ,  Z >. ,  Z >. } Z
) )  =  ( ( Z { <. <. Z ,  Z >. ,  Z >. } Z ) { <. <. Z ,  Z >. ,  Z >. }  ( Z { <. <. Z ,  Z >. ,  Z >. } Z
) ) ) )
93 oveq2 5876 . . . . . . . 8  |-  ( c  =  Z  ->  (
( Z { <. <. Z ,  Z >. ,  Z >. } Z ) { <. <. Z ,  Z >. ,  Z >. } c )  =  ( ( Z { <. <. Z ,  Z >. ,  Z >. } Z ) { <. <. Z ,  Z >. ,  Z >. } Z ) )
9489, 89oveq12d 5886 . . . . . . . 8  |-  ( c  =  Z  ->  (
( Z { <. <. Z ,  Z >. ,  Z >. } c ) { <. <. Z ,  Z >. ,  Z >. }  ( Z { <. <. Z ,  Z >. ,  Z >. } c ) )  =  ( ( Z { <. <. Z ,  Z >. ,  Z >. } Z ) { <. <. Z ,  Z >. ,  Z >. }  ( Z { <. <. Z ,  Z >. ,  Z >. } Z
) ) )
9593, 94eqeq12d 2192 . . . . . . 7  |-  ( c  =  Z  ->  (
( ( Z { <. <. Z ,  Z >. ,  Z >. } Z
) { <. <. Z ,  Z >. ,  Z >. } c )  =  ( ( Z { <. <. Z ,  Z >. ,  Z >. } c ) { <. <. Z ,  Z >. ,  Z >. }  ( Z { <. <. Z ,  Z >. ,  Z >. } c ) )  <->  ( ( Z { <. <. Z ,  Z >. ,  Z >. } Z
) { <. <. Z ,  Z >. ,  Z >. } Z )  =  ( ( Z { <. <. Z ,  Z >. ,  Z >. } Z ) { <. <. Z ,  Z >. ,  Z >. }  ( Z { <. <. Z ,  Z >. ,  Z >. } Z
) ) ) )
9692, 95anbi12d 473 . . . . . 6  |-  ( c  =  Z  ->  (
( ( Z { <. <. Z ,  Z >. ,  Z >. }  ( Z { <. <. Z ,  Z >. ,  Z >. } c ) )  =  ( ( Z { <. <. Z ,  Z >. ,  Z >. } Z ) { <. <. Z ,  Z >. ,  Z >. }  ( Z { <. <. Z ,  Z >. ,  Z >. } c ) )  /\  (
( Z { <. <. Z ,  Z >. ,  Z >. } Z ) { <. <. Z ,  Z >. ,  Z >. } c )  =  ( ( Z { <. <. Z ,  Z >. ,  Z >. } c ) { <. <. Z ,  Z >. ,  Z >. }  ( Z { <. <. Z ,  Z >. ,  Z >. } c ) ) )  <->  ( ( Z { <. <. Z ,  Z >. ,  Z >. }  ( Z { <. <. Z ,  Z >. ,  Z >. } Z
) )  =  ( ( Z { <. <. Z ,  Z >. ,  Z >. } Z ) { <. <. Z ,  Z >. ,  Z >. }  ( Z { <. <. Z ,  Z >. ,  Z >. } Z
) )  /\  (
( Z { <. <. Z ,  Z >. ,  Z >. } Z ) { <. <. Z ,  Z >. ,  Z >. } Z
)  =  ( ( Z { <. <. Z ,  Z >. ,  Z >. } Z ) { <. <. Z ,  Z >. ,  Z >. }  ( Z { <. <. Z ,  Z >. ,  Z >. } Z
) ) ) ) )
9796ralsng 3631 . . . . 5  |-  ( Z  e.  V  ->  ( A. c  e.  { Z }  ( ( Z { <. <. Z ,  Z >. ,  Z >. }  ( Z { <. <. Z ,  Z >. ,  Z >. } c ) )  =  ( ( Z { <. <. Z ,  Z >. ,  Z >. } Z ) { <. <. Z ,  Z >. ,  Z >. }  ( Z { <. <. Z ,  Z >. ,  Z >. } c ) )  /\  (
( Z { <. <. Z ,  Z >. ,  Z >. } Z ) { <. <. Z ,  Z >. ,  Z >. } c )  =  ( ( Z { <. <. Z ,  Z >. ,  Z >. } c ) { <. <. Z ,  Z >. ,  Z >. }  ( Z { <. <. Z ,  Z >. ,  Z >. } c ) ) )  <->  ( ( Z { <. <. Z ,  Z >. ,  Z >. }  ( Z { <. <. Z ,  Z >. ,  Z >. } Z
) )  =  ( ( Z { <. <. Z ,  Z >. ,  Z >. } Z ) { <. <. Z ,  Z >. ,  Z >. }  ( Z { <. <. Z ,  Z >. ,  Z >. } Z
) )  /\  (
( Z { <. <. Z ,  Z >. ,  Z >. } Z ) { <. <. Z ,  Z >. ,  Z >. } Z
)  =  ( ( Z { <. <. Z ,  Z >. ,  Z >. } Z ) { <. <. Z ,  Z >. ,  Z >. }  ( Z { <. <. Z ,  Z >. ,  Z >. } Z
) ) ) ) )
9877, 88, 973bitrd 214 . . . 4  |-  ( Z  e.  V  ->  ( A. a  e.  { Z } A. b  e.  { Z } A. c  e. 
{ Z }  (
( a { <. <. Z ,  Z >. ,  Z >. }  ( b { <. <. Z ,  Z >. ,  Z >. } c ) )  =  ( ( a { <. <. Z ,  Z >. ,  Z >. } b ) { <. <. Z ,  Z >. ,  Z >. }  (
a { <. <. Z ,  Z >. ,  Z >. } c ) )  /\  ( ( a {
<. <. Z ,  Z >. ,  Z >. } b ) { <. <. Z ,  Z >. ,  Z >. } c )  =  ( ( a { <. <. Z ,  Z >. ,  Z >. } c ) { <. <. Z ,  Z >. ,  Z >. }  (
b { <. <. Z ,  Z >. ,  Z >. } c ) ) )  <-> 
( ( Z { <. <. Z ,  Z >. ,  Z >. }  ( Z { <. <. Z ,  Z >. ,  Z >. } Z
) )  =  ( ( Z { <. <. Z ,  Z >. ,  Z >. } Z ) { <. <. Z ,  Z >. ,  Z >. }  ( Z { <. <. Z ,  Z >. ,  Z >. } Z
) )  /\  (
( Z { <. <. Z ,  Z >. ,  Z >. } Z ) { <. <. Z ,  Z >. ,  Z >. } Z
)  =  ( ( Z { <. <. Z ,  Z >. ,  Z >. } Z ) { <. <. Z ,  Z >. ,  Z >. }  ( Z { <. <. Z ,  Z >. ,  Z >. } Z
) ) ) ) )
9964, 66, 98mpbir2and 944 . . 3  |-  ( Z  e.  V  ->  A. a  e.  { Z } A. b  e.  { Z } A. c  e.  { Z }  ( (
a { <. <. Z ,  Z >. ,  Z >. }  ( b { <. <. Z ,  Z >. ,  Z >. } c ) )  =  ( ( a { <. <. Z ,  Z >. ,  Z >. } b ) { <. <. Z ,  Z >. ,  Z >. }  ( a { <. <. Z ,  Z >. ,  Z >. } c ) )  /\  (
( a { <. <. Z ,  Z >. ,  Z >. } b ) { <. <. Z ,  Z >. ,  Z >. } c )  =  ( ( a { <. <. Z ,  Z >. ,  Z >. } c ) { <. <. Z ,  Z >. ,  Z >. }  ( b { <. <. Z ,  Z >. ,  Z >. } c ) ) ) )
10038, 57, 993jca 1177 . 2  |-  ( Z  e.  V  ->  ( M  e.  Grp  /\  (mulGrp `  M )  e.  Mnd  /\ 
A. a  e.  { Z } A. b  e. 
{ Z } A. c  e.  { Z }  ( ( a { <. <. Z ,  Z >. ,  Z >. }  (
b { <. <. Z ,  Z >. ,  Z >. } c ) )  =  ( ( a {
<. <. Z ,  Z >. ,  Z >. } b ) { <. <. Z ,  Z >. ,  Z >. }  ( a { <. <. Z ,  Z >. ,  Z >. } c ) )  /\  ( ( a { <. <. Z ,  Z >. ,  Z >. } b ) { <. <. Z ,  Z >. ,  Z >. } c )  =  ( ( a { <. <. Z ,  Z >. ,  Z >. } c ) { <. <. Z ,  Z >. ,  Z >. }  ( b { <. <. Z ,  Z >. ,  Z >. } c ) ) ) ) )
101 eqidd 2178 . . . . . . . . . 10  |-  ( Z  e.  V  ->  a  =  a )
10213oveqd 5885 . . . . . . . . . 10  |-  ( Z  e.  V  ->  (
b { <. <. Z ,  Z >. ,  Z >. } c )  =  ( b ( +g  `  M
) c ) )
10348, 101, 102oveq123d 5889 . . . . . . . . 9  |-  ( Z  e.  V  ->  (
a { <. <. Z ,  Z >. ,  Z >. }  ( b { <. <. Z ,  Z >. ,  Z >. } c ) )  =  ( a ( .r `  M
) ( b ( +g  `  M ) c ) ) )
10448oveqd 5885 . . . . . . . . . 10  |-  ( Z  e.  V  ->  (
a { <. <. Z ,  Z >. ,  Z >. } b )  =  ( a ( .r `  M ) b ) )
10548oveqd 5885 . . . . . . . . . 10  |-  ( Z  e.  V  ->  (
a { <. <. Z ,  Z >. ,  Z >. } c )  =  ( a ( .r `  M ) c ) )
10613, 104, 105oveq123d 5889 . . . . . . . . 9  |-  ( Z  e.  V  ->  (
( a { <. <. Z ,  Z >. ,  Z >. } b ) { <. <. Z ,  Z >. ,  Z >. }  (
a { <. <. Z ,  Z >. ,  Z >. } c ) )  =  ( ( a ( .r `  M ) b ) ( +g  `  M ) ( a ( .r `  M
) c ) ) )
107103, 106eqeq12d 2192 . . . . . . . 8  |-  ( Z  e.  V  ->  (
( a { <. <. Z ,  Z >. ,  Z >. }  ( b { <. <. Z ,  Z >. ,  Z >. } c ) )  =  ( ( a { <. <. Z ,  Z >. ,  Z >. } b ) { <. <. Z ,  Z >. ,  Z >. }  (
a { <. <. Z ,  Z >. ,  Z >. } c ) )  <->  ( a
( .r `  M
) ( b ( +g  `  M ) c ) )  =  ( ( a ( .r `  M ) b ) ( +g  `  M ) ( a ( .r `  M
) c ) ) ) )
10813oveqd 5885 . . . . . . . . . 10  |-  ( Z  e.  V  ->  (
a { <. <. Z ,  Z >. ,  Z >. } b )  =  ( a ( +g  `  M
) b ) )
109 eqidd 2178 . . . . . . . . . 10  |-  ( Z  e.  V  ->  c  =  c )
11048, 108, 109oveq123d 5889 . . . . . . . . 9  |-  ( Z  e.  V  ->  (
( a { <. <. Z ,  Z >. ,  Z >. } b ) { <. <. Z ,  Z >. ,  Z >. } c )  =  ( ( a ( +g  `  M
) b ) ( .r `  M ) c ) )
11148oveqd 5885 . . . . . . . . . 10  |-  ( Z  e.  V  ->  (
b { <. <. Z ,  Z >. ,  Z >. } c )  =  ( b ( .r `  M ) c ) )
11213, 105, 111oveq123d 5889 . . . . . . . . 9  |-  ( Z  e.  V  ->  (
( a { <. <. Z ,  Z >. ,  Z >. } c ) { <. <. Z ,  Z >. ,  Z >. }  (
b { <. <. Z ,  Z >. ,  Z >. } c ) )  =  ( ( a ( .r `  M ) c ) ( +g  `  M ) ( b ( .r `  M
) c ) ) )
113110, 112eqeq12d 2192 . . . . . . . 8  |-  ( Z  e.  V  ->  (
( ( a {
<. <. Z ,  Z >. ,  Z >. } b ) { <. <. Z ,  Z >. ,  Z >. } c )  =  ( ( a { <. <. Z ,  Z >. ,  Z >. } c ) { <. <. Z ,  Z >. ,  Z >. }  (
b { <. <. Z ,  Z >. ,  Z >. } c ) )  <->  ( (
a ( +g  `  M
) b ) ( .r `  M ) c )  =  ( ( a ( .r
`  M ) c ) ( +g  `  M
) ( b ( .r `  M ) c ) ) ) )
114107, 113anbi12d 473 . . . . . . 7  |-  ( Z  e.  V  ->  (
( ( a {
<. <. Z ,  Z >. ,  Z >. }  (
b { <. <. Z ,  Z >. ,  Z >. } c ) )  =  ( ( a {
<. <. Z ,  Z >. ,  Z >. } b ) { <. <. Z ,  Z >. ,  Z >. }  ( a { <. <. Z ,  Z >. ,  Z >. } c ) )  /\  ( ( a { <. <. Z ,  Z >. ,  Z >. } b ) { <. <. Z ,  Z >. ,  Z >. } c )  =  ( ( a { <. <. Z ,  Z >. ,  Z >. } c ) { <. <. Z ,  Z >. ,  Z >. }  ( b { <. <. Z ,  Z >. ,  Z >. } c ) ) )  <->  ( (
a ( .r `  M ) ( b ( +g  `  M
) c ) )  =  ( ( a ( .r `  M
) b ) ( +g  `  M ) ( a ( .r
`  M ) c ) )  /\  (
( a ( +g  `  M ) b ) ( .r `  M
) c )  =  ( ( a ( .r `  M ) c ) ( +g  `  M ) ( b ( .r `  M
) c ) ) ) ) )
11510, 114raleqbidv 2684 . . . . . 6  |-  ( Z  e.  V  ->  ( A. c  e.  { Z }  ( ( a { <. <. Z ,  Z >. ,  Z >. }  (
b { <. <. Z ,  Z >. ,  Z >. } c ) )  =  ( ( a {
<. <. Z ,  Z >. ,  Z >. } b ) { <. <. Z ,  Z >. ,  Z >. }  ( a { <. <. Z ,  Z >. ,  Z >. } c ) )  /\  ( ( a { <. <. Z ,  Z >. ,  Z >. } b ) { <. <. Z ,  Z >. ,  Z >. } c )  =  ( ( a { <. <. Z ,  Z >. ,  Z >. } c ) { <. <. Z ,  Z >. ,  Z >. }  ( b { <. <. Z ,  Z >. ,  Z >. } c ) ) )  <->  A. c  e.  ( Base `  M
) ( ( a ( .r `  M
) ( b ( +g  `  M ) c ) )  =  ( ( a ( .r `  M ) b ) ( +g  `  M ) ( a ( .r `  M
) c ) )  /\  ( ( a ( +g  `  M
) b ) ( .r `  M ) c )  =  ( ( a ( .r
`  M ) c ) ( +g  `  M
) ( b ( .r `  M ) c ) ) ) ) )
11610, 115raleqbidv 2684 . . . . 5  |-  ( Z  e.  V  ->  ( A. b  e.  { Z } A. c  e.  { Z }  ( (
a { <. <. Z ,  Z >. ,  Z >. }  ( b { <. <. Z ,  Z >. ,  Z >. } c ) )  =  ( ( a { <. <. Z ,  Z >. ,  Z >. } b ) { <. <. Z ,  Z >. ,  Z >. }  ( a { <. <. Z ,  Z >. ,  Z >. } c ) )  /\  (
( a { <. <. Z ,  Z >. ,  Z >. } b ) { <. <. Z ,  Z >. ,  Z >. } c )  =  ( ( a { <. <. Z ,  Z >. ,  Z >. } c ) { <. <. Z ,  Z >. ,  Z >. }  ( b { <. <. Z ,  Z >. ,  Z >. } c ) ) )  <->  A. b  e.  ( Base `  M
) A. c  e.  ( Base `  M
) ( ( a ( .r `  M
) ( b ( +g  `  M ) c ) )  =  ( ( a ( .r `  M ) b ) ( +g  `  M ) ( a ( .r `  M
) c ) )  /\  ( ( a ( +g  `  M
) b ) ( .r `  M ) c )  =  ( ( a ( .r
`  M ) c ) ( +g  `  M
) ( b ( .r `  M ) c ) ) ) ) )
11710, 116raleqbidv 2684 . . . 4  |-  ( Z  e.  V  ->  ( A. a  e.  { Z } A. b  e.  { Z } A. c  e. 
{ Z }  (
( a { <. <. Z ,  Z >. ,  Z >. }  ( b { <. <. Z ,  Z >. ,  Z >. } c ) )  =  ( ( a { <. <. Z ,  Z >. ,  Z >. } b ) { <. <. Z ,  Z >. ,  Z >. }  (
a { <. <. Z ,  Z >. ,  Z >. } c ) )  /\  ( ( a {
<. <. Z ,  Z >. ,  Z >. } b ) { <. <. Z ,  Z >. ,  Z >. } c )  =  ( ( a { <. <. Z ,  Z >. ,  Z >. } c ) { <. <. Z ,  Z >. ,  Z >. }  (
b { <. <. Z ,  Z >. ,  Z >. } c ) ) )  <->  A. a  e.  ( Base `  M ) A. b  e.  ( Base `  M ) A. c  e.  ( Base `  M
) ( ( a ( .r `  M
) ( b ( +g  `  M ) c ) )  =  ( ( a ( .r `  M ) b ) ( +g  `  M ) ( a ( .r `  M
) c ) )  /\  ( ( a ( +g  `  M
) b ) ( .r `  M ) c )  =  ( ( a ( .r
`  M ) c ) ( +g  `  M
) ( b ( .r `  M ) c ) ) ) ) )
1181173anbi3d 1318 . . 3  |-  ( Z  e.  V  ->  (
( M  e.  Grp  /\  (mulGrp `  M )  e.  Mnd  /\  A. a  e.  { Z } A. b  e.  { Z } A. c  e.  { Z }  ( (
a { <. <. Z ,  Z >. ,  Z >. }  ( b { <. <. Z ,  Z >. ,  Z >. } c ) )  =  ( ( a { <. <. Z ,  Z >. ,  Z >. } b ) { <. <. Z ,  Z >. ,  Z >. }  ( a { <. <. Z ,  Z >. ,  Z >. } c ) )  /\  (
( a { <. <. Z ,  Z >. ,  Z >. } b ) { <. <. Z ,  Z >. ,  Z >. } c )  =  ( ( a { <. <. Z ,  Z >. ,  Z >. } c ) { <. <. Z ,  Z >. ,  Z >. }  ( b { <. <. Z ,  Z >. ,  Z >. } c ) ) ) )  <-> 
( M  e.  Grp  /\  (mulGrp `  M )  e.  Mnd  /\  A. a  e.  ( Base `  M
) A. b  e.  ( Base `  M
) A. c  e.  ( Base `  M
) ( ( a ( .r `  M
) ( b ( +g  `  M ) c ) )  =  ( ( a ( .r `  M ) b ) ( +g  `  M ) ( a ( .r `  M
) c ) )  /\  ( ( a ( +g  `  M
) b ) ( .r `  M ) c )  =  ( ( a ( .r
`  M ) c ) ( +g  `  M
) ( b ( .r `  M ) c ) ) ) ) ) )
11933, 43, 34, 51isring 12996 . . 3  |-  ( M  e.  Ring  <->  ( M  e. 
Grp  /\  (mulGrp `  M
)  e.  Mnd  /\  A. a  e.  ( Base `  M ) A. b  e.  ( Base `  M
) A. c  e.  ( Base `  M
) ( ( a ( .r `  M
) ( b ( +g  `  M ) c ) )  =  ( ( a ( .r `  M ) b ) ( +g  `  M ) ( a ( .r `  M
) c ) )  /\  ( ( a ( +g  `  M
) b ) ( .r `  M ) c )  =  ( ( a ( .r
`  M ) c ) ( +g  `  M
) ( b ( .r `  M ) c ) ) ) ) )
120118, 119bitr4di 198 . 2  |-  ( Z  e.  V  ->  (
( M  e.  Grp  /\  (mulGrp `  M )  e.  Mnd  /\  A. a  e.  { Z } A. b  e.  { Z } A. c  e.  { Z }  ( (
a { <. <. Z ,  Z >. ,  Z >. }  ( b { <. <. Z ,  Z >. ,  Z >. } c ) )  =  ( ( a { <. <. Z ,  Z >. ,  Z >. } b ) { <. <. Z ,  Z >. ,  Z >. }  ( a { <. <. Z ,  Z >. ,  Z >. } c ) )  /\  (
( a { <. <. Z ,  Z >. ,  Z >. } b ) { <. <. Z ,  Z >. ,  Z >. } c )  =  ( ( a { <. <. Z ,  Z >. ,  Z >. } c ) { <. <. Z ,  Z >. ,  Z >. }  ( b { <. <. Z ,  Z >. ,  Z >. } c ) ) ) )  <-> 
M  e.  Ring )
)
121100, 120mpbid 147 1  |-  ( Z  e.  V  ->  M  e.  Ring )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 104    <-> wb 105    /\ w3a 978    = wceq 1353    e. wcel 2148   A.wral 2455   _Vcvv 2737   {csn 3591   {cpr 3592   {ctp 3593   <.cop 3594   ` cfv 5211  (class class class)co 5868   NNcn 8895   ndxcnx 12429  Slot cslot 12431   Basecbs 12432   +g cplusg 12505   .rcmulr 12506   Mndcmnd 12696   Grpcgrp 12754  mulGrpcmgp 12944   Ringcrg 12992
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-in1 614  ax-in2 615  ax-io 709  ax-5 1447  ax-7 1448  ax-gen 1449  ax-ie1 1493  ax-ie2 1494  ax-8 1504  ax-10 1505  ax-11 1506  ax-i12 1507  ax-bndl 1509  ax-4 1510  ax-17 1526  ax-i9 1530  ax-ial 1534  ax-i5r 1535  ax-13 2150  ax-14 2151  ax-ext 2159  ax-sep 4118  ax-pow 4171  ax-pr 4205  ax-un 4429  ax-setind 4532  ax-cnex 7880  ax-resscn 7881  ax-1cn 7882  ax-1re 7883  ax-icn 7884  ax-addcl 7885  ax-addrcl 7886  ax-mulcl 7887  ax-addcom 7889  ax-addass 7891  ax-distr 7893  ax-i2m1 7894  ax-0lt1 7895  ax-0id 7897  ax-rnegex 7898  ax-cnre 7900  ax-pre-ltirr 7901  ax-pre-ltwlin 7902  ax-pre-lttrn 7903  ax-pre-apti 7904  ax-pre-ltadd 7905
This theorem depends on definitions:  df-bi 117  df-3or 979  df-3an 980  df-tru 1356  df-fal 1359  df-nf 1461  df-sb 1763  df-eu 2029  df-mo 2030  df-clab 2164  df-cleq 2170  df-clel 2173  df-nfc 2308  df-ne 2348  df-nel 2443  df-ral 2460  df-rex 2461  df-reu 2462  df-rmo 2463  df-rab 2464  df-v 2739  df-sbc 2963  df-csb 3058  df-dif 3131  df-un 3133  df-in 3135  df-ss 3142  df-nul 3423  df-pw 3576  df-sn 3597  df-pr 3598  df-tp 3599  df-op 3600  df-uni 3808  df-int 3843  df-br 4001  df-opab 4062  df-mpt 4063  df-id 4289  df-xp 4628  df-rel 4629  df-cnv 4630  df-co 4631  df-dm 4632  df-rn 4633  df-res 4634  df-ima 4635  df-iota 5173  df-fun 5213  df-fn 5214  df-f 5215  df-fv 5219  df-riota 5824  df-ov 5871  df-oprab 5872  df-mpo 5873  df-pnf 7971  df-mnf 7972  df-xr 7973  df-ltxr 7974  df-le 7975  df-sub 8107  df-neg 8108  df-inn 8896  df-2 8954  df-3 8955  df-n0 9153  df-z 9230  df-uz 9505  df-fz 9983  df-struct 12434  df-ndx 12435  df-slot 12436  df-base 12438  df-sets 12439  df-plusg 12518  df-mulr 12519  df-0g 12642  df-mgm 12654  df-sgrp 12687  df-mnd 12697  df-grp 12757  df-mgp 12945  df-ring 12994
This theorem is referenced by:  ringn0  13050
  Copyright terms: Public domain W3C validator