ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  rngpropd Unicode version
Theorem rngpropd 13832
Description: If two structures have the same base set, and the values of their group (addition) and ring (multiplication) operations are equal for all pairs of elements of the base set, one is a non-unital ring iff the other one is. (Contributed by AV, 15-Feb-2025.)
Hypotheses
Ref Expression
rngpropd.1 |- ( ph -> B = ( Base ` K ) )
rngpropd.2 |- ( ph -> B = ( Base ` L ) )
rngpropd.3 |- ( ( ph /\ ( x e. B /\ y e. B ) ) -> ( x ( +g ` K ) y ) = ( x ( +g ` L ) y ) )
rngpropd.4 |- ( ( ph /\ ( x e. B /\ y e. B ) ) -> ( x ( .r ` K ) y ) = ( x ( .r ` L ) y ) )
Assertion
Ref Expression
rngpropd |- ( ph -> ( K e. Rng <-> L e. Rng ) )
Distinct variable groups:   x, y, B   x, K, y   ph, x, y   x, L, y
Proof of Theorem rngpropd
Dummy variables v u w are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 simpll 527 . . . . . . . . . . . . 13 |- ( ( ( ph /\ ( K e. Abel /\ (mulGrp ` K ) e. Smgrp ) ) /\ ( ( u e. B /\ v e. B ) /\ w e. B ) ) -> ph )
2 simprll 537 . . . . . . . . . . . . 13 |- ( ( ( ph /\ ( K e. Abel /\ (mulGrp ` K ) e. Smgrp ) ) /\ ( ( u e. B /\ v e. B ) /\ w e. B ) ) -> u e. B )
3 simplrl 535 . . . . . . . . . . . . . . 15 |- ( ( ( ph /\ ( K e. Abel /\ (mulGrp ` K ) e. Smgrp ) ) /\ ( ( u e. B /\ v e. B ) /\ w e. B ) ) -> K e. Abel )
4 simprlr 538 . . . . . . . . . . . . . . . 16 |- ( ( ( ph /\ ( K e. Abel /\ (mulGrp ` K ) e. Smgrp ) ) /\ ( ( u e. B /\ v e. B ) /\ w e. B ) ) -> v e. B )
5 rngpropd.1 . . . . . . . . . . . . . . . . 17 |- ( ph -> B = ( Base ` K ) )
65ad2antrr 488 . . . . . . . . . . . . . . . 16 |- ( ( ( ph /\ ( K e. Abel /\ (mulGrp ` K ) e. Smgrp ) ) /\ ( ( u e. B /\ v e. B ) /\ w e. B ) ) -> B = ( Base ` K ) )
74, 6eleqtrd 2286 . . . . . . . . . . . . . . 15 |- ( ( ( ph /\ ( K e. Abel /\ (mulGrp ` K ) e. Smgrp ) ) /\ ( ( u e. B /\ v e. B ) /\ w e. B ) ) -> v e. ( Base ` K ) )
8 simprr 531 . . . . . . . . . . . . . . . 16 |- ( ( ( ph /\ ( K e. Abel /\ (mulGrp ` K ) e. Smgrp ) ) /\ ( ( u e. B /\ v e. B ) /\ w e. B ) ) -> w e. B )
98, 6eleqtrd 2286 . . . . . . . . . . . . . . 15 |- ( ( ( ph /\ ( K e. Abel /\ (mulGrp ` K ) e. Smgrp ) ) /\ ( ( u e. B /\ v e. B ) /\ w e. B ) ) -> w e. ( Base ` K ) )
10 ablgrp 13740 . . . . . . . . . . . . . . . 16 |- ( K e. Abel -> K e. Grp )
11 eqid 2207 . . . . . . . . . . . . . . . . 17 |- ( Base ` K ) = ( Base ` K )
12 eqid 2207 . . . . . . . . . . . . . . . . 17 |- ( +g ` K ) = ( +g ` K )
1311, 12grpcl 13455 . . . . . . . . . . . . . . . 16 |- ( ( K e. Grp /\ v e. ( Base ` K ) /\ w e. ( Base ` K ) ) -> ( v ( +g ` K ) w ) e. ( Base ` K ) )
1410, 13syl3an1 1283 . . . . . . . . . . . . . . 15 |- ( ( K e. Abel /\ v e. ( Base ` K ) /\ w e. ( Base ` K ) ) -> ( v ( +g ` K ) w ) e. ( Base ` K ) )
153, 7, 9, 14syl3anc 1250 . . . . . . . . . . . . . 14 |- ( ( ( ph /\ ( K e. Abel /\ (mulGrp ` K ) e. Smgrp ) ) /\ ( ( u e. B /\ v e. B ) /\ w e. B ) ) -> ( v ( +g ` K ) w ) e. ( Base ` K ) )
1615, 6eleqtrrd 2287 . . . . . . . . . . . . 13 |- ( ( ( ph /\ ( K e. Abel /\ (mulGrp ` K ) e. Smgrp ) ) /\ ( ( u e. B /\ v e. B ) /\ w e. B ) ) -> ( v ( +g ` K ) w ) e. B )
17 rngpropd.4 . . . . . . . . . . . . . 14 |- ( ( ph /\ ( x e. B /\ y e. B ) ) -> ( x ( .r ` K ) y ) = ( x ( .r ` L ) y ) )
1817oveqrspc2v 5994 . . . . . . . . . . . . 13 |- ( ( ph /\ ( u e. B /\ ( v ( +g ` K ) w ) e. B ) ) -> ( u ( .r ` K ) ( v ( +g ` K ) w ) ) = ( u ( .r ` L ) ( v ( +g ` K ) w ) ) )
191, 2, 16, 18syl12anc 1248 . . . . . . . . . . . 12 |- ( ( ( ph /\ ( K e. Abel /\ (mulGrp ` K ) e. Smgrp ) ) /\ ( ( u e. B /\ v e. B ) /\ w e. B ) ) -> ( u ( .r ` K ) ( v ( +g ` K ) w ) ) = ( u ( .r ` L ) ( v ( +g ` K ) w ) ) )
20 rngpropd.3 . . . . . . . . . . . . . . 15 |- ( ( ph /\ ( x e. B /\ y e. B ) ) -> ( x ( +g ` K ) y ) = ( x ( +g ` L ) y ) )
2120oveqrspc2v 5994 . . . . . . . . . . . . . 14 |- ( ( ph /\ ( v e. B /\ w e. B ) ) -> ( v ( +g ` K ) w ) = ( v ( +g ` L ) w ) )
221, 4, 8, 21syl12anc 1248 . . . . . . . . . . . . 13 |- ( ( ( ph /\ ( K e. Abel /\ (mulGrp ` K ) e. Smgrp ) ) /\ ( ( u e. B /\ v e. B ) /\ w e. B ) ) -> ( v ( +g ` K ) w ) = ( v ( +g ` L ) w ) )
2322oveq2d 5983 . . . . . . . . . . . 12 |- ( ( ( ph /\ ( K e. Abel /\ (mulGrp ` K ) e. Smgrp ) ) /\ ( ( u e. B /\ v e. B ) /\ w e. B ) ) -> ( u ( .r ` L ) ( v ( +g ` K ) w ) ) = ( u ( .r ` L ) ( v ( +g ` L ) w ) ) )
2419, 23eqtrd 2240 . . . . . . . . . . 11 |- ( ( ( ph /\ ( K e. Abel /\ (mulGrp ` K ) e. Smgrp ) ) /\ ( ( u e. B /\ v e. B ) /\ w e. B ) ) -> ( u ( .r ` K ) ( v ( +g ` K ) w ) ) = ( u ( .r ` L ) ( v ( +g ` L ) w ) ) )
25 simplrr 536 . . . . . . . . . . . . . . . 16 |- ( ( ( ph /\ ( K e. Abel /\ (mulGrp ` K ) e. Smgrp ) ) /\ ( ( u e. B /\ v e. B ) /\ w e. B ) ) -> (mulGrp ` K ) e. Smgrp )
262, 6eleqtrd 2286 . . . . . . . . . . . . . . . . 17 |- ( ( ( ph /\ ( K e. Abel /\ (mulGrp ` K ) e. Smgrp ) ) /\ ( ( u e. B /\ v e. B ) /\ w e. B ) ) -> u e. ( Base ` K ) )
273elexd 2790 . . . . . . . . . . . . . . . . . 18 |- ( ( ( ph /\ ( K e. Abel /\ (mulGrp ` K ) e. Smgrp ) ) /\ ( ( u e. B /\ v e. B ) /\ w e. B ) ) -> K e. _V )
28 eqid 2207 . . . . . . . . . . . . . . . . . . 19 |- (mulGrp ` K ) = (mulGrp ` K )
2928, 11mgpbasg 13803 . . . . . . . . . . . . . . . . . 18 |- ( K e. _V -> ( Base ` K ) = ( Base ` (mulGrp ` K ) ) )
3027, 29syl 14 . . . . . . . . . . . . . . . . 17 |- ( ( ( ph /\ ( K e. Abel /\ (mulGrp ` K ) e. Smgrp ) ) /\ ( ( u e. B /\ v e. B ) /\ w e. B ) ) -> ( Base ` K ) = ( Base ` (mulGrp ` K ) ) )
3126, 30eleqtrd 2286 . . . . . . . . . . . . . . . 16 |- ( ( ( ph /\ ( K e. Abel /\ (mulGrp ` K ) e. Smgrp ) ) /\ ( ( u e. B /\ v e. B ) /\ w e. B ) ) -> u e. ( Base ` (mulGrp ` K ) ) )
327, 30eleqtrd 2286 . . . . . . . . . . . . . . . 16 |- ( ( ( ph /\ ( K e. Abel /\ (mulGrp ` K ) e. Smgrp ) ) /\ ( ( u e. B /\ v e. B ) /\ w e. B ) ) -> v e. ( Base ` (mulGrp ` K ) ) )
33 eqid 2207 . . . . . . . . . . . . . . . . 17 |- ( Base ` (mulGrp ` K ) ) = ( Base ` (mulGrp ` K ) )
34 eqid 2207 . . . . . . . . . . . . . . . . 17 |- ( +g ` (mulGrp ` K ) ) = ( +g ` (mulGrp ` K ) )
3533, 34sgrpcl 13356 . . . . . . . . . . . . . . . 16 |- ( ( (mulGrp ` K ) e. Smgrp /\ u e. ( Base ` (mulGrp ` K ) ) /\ v e. ( Base ` (mulGrp ` K ) ) ) -> ( u ( +g ` (mulGrp ` K ) ) v ) e. ( Base ` (mulGrp ` K ) ) )
3625, 31, 32, 35syl3anc 1250 . . . . . . . . . . . . . . 15 |- ( ( ( ph /\ ( K e. Abel /\ (mulGrp ` K ) e. Smgrp ) ) /\ ( ( u e. B /\ v e. B ) /\ w e. B ) ) -> ( u ( +g ` (mulGrp ` K ) ) v ) e. ( Base ` (mulGrp ` K ) ) )
37 eqid 2207 . . . . . . . . . . . . . . . . . 18 |- ( .r ` K ) = ( .r ` K )
3828, 37mgpplusgg 13801 . . . . . . . . . . . . . . . . 17 |- ( K e. _V -> ( .r ` K ) = ( +g ` (mulGrp ` K ) ) )
3927, 38syl 14 . . . . . . . . . . . . . . . 16 |- ( ( ( ph /\ ( K e. Abel /\ (mulGrp ` K ) e. Smgrp ) ) /\ ( ( u e. B /\ v e. B ) /\ w e. B ) ) -> ( .r ` K ) = ( +g ` (mulGrp ` K ) ) )
4039oveqd 5984 . . . . . . . . . . . . . . 15 |- ( ( ( ph /\ ( K e. Abel /\ (mulGrp ` K ) e. Smgrp ) ) /\ ( ( u e. B /\ v e. B ) /\ w e. B ) ) -> ( u ( .r ` K ) v ) = ( u ( +g ` (mulGrp ` K ) ) v ) )
4136, 40, 303eltr4d 2291 . . . . . . . . . . . . . 14 |- ( ( ( ph /\ ( K e. Abel /\ (mulGrp ` K ) e. Smgrp ) ) /\ ( ( u e. B /\ v e. B ) /\ w e. B ) ) -> ( u ( .r ` K ) v ) e. ( Base ` K ) )
4241, 6eleqtrrd 2287 . . . . . . . . . . . . 13 |- ( ( ( ph /\ ( K e. Abel /\ (mulGrp ` K ) e. Smgrp ) ) /\ ( ( u e. B /\ v e. B ) /\ w e. B ) ) -> ( u ( .r ` K ) v ) e. B )
439, 30eleqtrd 2286 . . . . . . . . . . . . . . . 16 |- ( ( ( ph /\ ( K e. Abel /\ (mulGrp ` K ) e. Smgrp ) ) /\ ( ( u e. B /\ v e. B ) /\ w e. B ) ) -> w e. ( Base ` (mulGrp ` K ) ) )
4433, 34sgrpcl 13356 . . . . . . . . . . . . . . . 16 |- ( ( (mulGrp ` K ) e. Smgrp /\ u e. ( Base ` (mulGrp ` K ) ) /\ w e. ( Base ` (mulGrp ` K ) ) ) -> ( u ( +g ` (mulGrp ` K ) ) w ) e. ( Base ` (mulGrp ` K ) ) )
4525, 31, 43, 44syl3anc 1250 . . . . . . . . . . . . . . 15 |- ( ( ( ph /\ ( K e. Abel /\ (mulGrp ` K ) e. Smgrp ) ) /\ ( ( u e. B /\ v e. B ) /\ w e. B ) ) -> ( u ( +g ` (mulGrp ` K ) ) w ) e. ( Base ` (mulGrp ` K ) ) )
4639oveqd 5984 . . . . . . . . . . . . . . 15 |- ( ( ( ph /\ ( K e. Abel /\ (mulGrp ` K ) e. Smgrp ) ) /\ ( ( u e. B /\ v e. B ) /\ w e. B ) ) -> ( u ( .r ` K ) w ) = ( u ( +g ` (mulGrp ` K ) ) w ) )
4745, 46, 303eltr4d 2291 . . . . . . . . . . . . . 14 |- ( ( ( ph /\ ( K e. Abel /\ (mulGrp ` K ) e. Smgrp ) ) /\ ( ( u e. B /\ v e. B ) /\ w e. B ) ) -> ( u ( .r ` K ) w ) e. ( Base ` K ) )
4847, 6eleqtrrd 2287 . . . . . . . . . . . . 13 |- ( ( ( ph /\ ( K e. Abel /\ (mulGrp ` K ) e. Smgrp ) ) /\ ( ( u e. B /\ v e. B ) /\ w e. B ) ) -> ( u ( .r ` K ) w ) e. B )
4920oveqrspc2v 5994 . . . . . . . . . . . . 13 |- ( ( ph /\ ( ( u ( .r ` K ) v ) e. B /\ ( u ( .r ` K ) w ) e. B ) ) -> ( ( u ( .r ` K ) v ) ( +g ` K ) ( u ( .r ` K ) w ) ) = ( ( u ( .r ` K ) v ) ( +g ` L ) ( u ( .r ` K ) w ) ) )
501, 42, 48, 49syl12anc 1248 . . . . . . . . . . . 12 |- ( ( ( ph /\ ( K e. Abel /\ (mulGrp ` K ) e. Smgrp ) ) /\ ( ( u e. B /\ v e. B ) /\ w e. B ) ) -> ( ( u ( .r ` K ) v ) ( +g ` K ) ( u ( .r ` K ) w ) ) = ( ( u ( .r ` K ) v ) ( +g ` L ) ( u ( .r ` K ) w ) ) )
5117oveqrspc2v 5994 . . . . . . . . . . . . . 14 |- ( ( ph /\ ( u e. B /\ v e. B ) ) -> ( u ( .r ` K ) v ) = ( u ( .r ` L ) v ) )
5251ad2ant2r 509 . . . . . . . . . . . . 13 |- ( ( ( ph /\ ( K e. Abel /\ (mulGrp ` K ) e. Smgrp ) ) /\ ( ( u e. B /\ v e. B ) /\ w e. B ) ) -> ( u ( .r ` K ) v ) = ( u ( .r ` L ) v ) )
5317oveqrspc2v 5994 . . . . . . . . . . . . . 14 |- ( ( ph /\ ( u e. B /\ w e. B ) ) -> ( u ( .r ` K ) w ) = ( u ( .r ` L ) w ) )
541, 2, 8, 53syl12anc 1248 . . . . . . . . . . . . 13 |- ( ( ( ph /\ ( K e. Abel /\ (mulGrp ` K ) e. Smgrp ) ) /\ ( ( u e. B /\ v e. B ) /\ w e. B ) ) -> ( u ( .r ` K ) w ) = ( u ( .r ` L ) w ) )
5552, 54oveq12d 5985 . . . . . . . . . . . 12 |- ( ( ( ph /\ ( K e. Abel /\ (mulGrp ` K ) e. Smgrp ) ) /\ ( ( u e. B /\ v e. B ) /\ w e. B ) ) -> ( ( u ( .r ` K ) v ) ( +g ` L ) ( u ( .r ` K ) w ) ) = ( ( u ( .r ` L ) v ) ( +g ` L ) ( u ( .r ` L ) w ) ) )
5650, 55eqtrd 2240 . . . . . . . . . . 11 |- ( ( ( ph /\ ( K e. Abel /\ (mulGrp ` K ) e. Smgrp ) ) /\ ( ( u e. B /\ v e. B ) /\ w e. B ) ) -> ( ( u ( .r ` K ) v ) ( +g ` K ) ( u ( .r ` K ) w ) ) = ( ( u ( .r ` L ) v ) ( +g ` L ) ( u ( .r ` L ) w ) ) )
5724, 56eqeq12d 2222 . . . . . . . . . 10 |- ( ( ( ph /\ ( K e. Abel /\ (mulGrp ` K ) e. Smgrp ) ) /\ ( ( u e. B /\ v e. B ) /\ w e. B ) ) -> ( ( u ( .r ` K ) ( v ( +g ` K ) w ) ) = ( ( u ( .r ` K ) v ) ( +g ` K ) ( u ( .r ` K ) w ) ) <-> ( u ( .r ` L ) ( v ( +g ` L ) w ) ) = ( ( u ( .r ` L ) v ) ( +g ` L ) ( u ( .r ` L ) w ) ) ) )
5811, 12grpcl 13455 . . . . . . . . . . . . . . . 16 |- ( ( K e. Grp /\ u e. ( Base ` K ) /\ v e. ( Base ` K ) ) -> ( u ( +g ` K ) v ) e. ( Base ` K ) )
5910, 58syl3an1 1283 . . . . . . . . . . . . . . 15 |- ( ( K e. Abel /\ u e. ( Base ` K ) /\ v e. ( Base ` K ) ) -> ( u ( +g ` K ) v ) e. ( Base ` K ) )
603, 26, 7, 59syl3anc 1250 . . . . . . . . . . . . . 14 |- ( ( ( ph /\ ( K e. Abel /\ (mulGrp ` K ) e. Smgrp ) ) /\ ( ( u e. B /\ v e. B ) /\ w e. B ) ) -> ( u ( +g ` K ) v ) e. ( Base ` K ) )
6160, 6eleqtrrd 2287 . . . . . . . . . . . . 13 |- ( ( ( ph /\ ( K e. Abel /\ (mulGrp ` K ) e. Smgrp ) ) /\ ( ( u e. B /\ v e. B ) /\ w e. B ) ) -> ( u ( +g ` K ) v ) e. B )
6217oveqrspc2v 5994 . . . . . . . . . . . . 13 |- ( ( ph /\ ( ( u ( +g ` K ) v ) e. B /\ w e. B ) ) -> ( ( u ( +g ` K ) v ) ( .r ` K ) w ) = ( ( u ( +g ` K ) v ) ( .r ` L ) w ) )
631, 61, 8, 62syl12anc 1248 . . . . . . . . . . . 12 |- ( ( ( ph /\ ( K e. Abel /\ (mulGrp ` K ) e. Smgrp ) ) /\ ( ( u e. B /\ v e. B ) /\ w e. B ) ) -> ( ( u ( +g ` K ) v ) ( .r ` K ) w ) = ( ( u ( +g ` K ) v ) ( .r ` L ) w ) )
6420oveqrspc2v 5994 . . . . . . . . . . . . . 14 |- ( ( ph /\ ( u e. B /\ v e. B ) ) -> ( u ( +g ` K ) v ) = ( u ( +g ` L ) v ) )
6564ad2ant2r 509 . . . . . . . . . . . . 13 |- ( ( ( ph /\ ( K e. Abel /\ (mulGrp ` K ) e. Smgrp ) ) /\ ( ( u e. B /\ v e. B ) /\ w e. B ) ) -> ( u ( +g ` K ) v ) = ( u ( +g ` L ) v ) )
6665oveq1d 5982 . . . . . . . . . . . 12 |- ( ( ( ph /\ ( K e. Abel /\ (mulGrp ` K ) e. Smgrp ) ) /\ ( ( u e. B /\ v e. B ) /\ w e. B ) ) -> ( ( u ( +g ` K ) v ) ( .r ` L ) w ) = ( ( u ( +g ` L ) v ) ( .r ` L ) w ) )
6763, 66eqtrd 2240 . . . . . . . . . . 11 |- ( ( ( ph /\ ( K e. Abel /\ (mulGrp ` K ) e. Smgrp ) ) /\ ( ( u e. B /\ v e. B ) /\ w e. B ) ) -> ( ( u ( +g ` K ) v ) ( .r ` K ) w ) = ( ( u ( +g ` L ) v ) ( .r ` L ) w ) )
6833, 34sgrpcl 13356 . . . . . . . . . . . . . . . 16 |- ( ( (mulGrp ` K ) e. Smgrp /\ v e. ( Base ` (mulGrp ` K ) ) /\ w e. ( Base ` (mulGrp ` K ) ) ) -> ( v ( +g ` (mulGrp ` K ) ) w ) e. ( Base ` (mulGrp ` K ) ) )
6925, 32, 43, 68syl3anc 1250 . . . . . . . . . . . . . . 15 |- ( ( ( ph /\ ( K e. Abel /\ (mulGrp ` K ) e. Smgrp ) ) /\ ( ( u e. B /\ v e. B ) /\ w e. B ) ) -> ( v ( +g ` (mulGrp ` K ) ) w ) e. ( Base ` (mulGrp ` K ) ) )
7039oveqd 5984 . . . . . . . . . . . . . . 15 |- ( ( ( ph /\ ( K e. Abel /\ (mulGrp ` K ) e. Smgrp ) ) /\ ( ( u e. B /\ v e. B ) /\ w e. B ) ) -> ( v ( .r ` K ) w ) = ( v ( +g ` (mulGrp ` K ) ) w ) )
7169, 70, 303eltr4d 2291 . . . . . . . . . . . . . 14 |- ( ( ( ph /\ ( K e. Abel /\ (mulGrp ` K ) e. Smgrp ) ) /\ ( ( u e. B /\ v e. B ) /\ w e. B ) ) -> ( v ( .r ` K ) w ) e. ( Base ` K ) )
7271, 6eleqtrrd 2287 . . . . . . . . . . . . 13 |- ( ( ( ph /\ ( K e. Abel /\ (mulGrp ` K ) e. Smgrp ) ) /\ ( ( u e. B /\ v e. B ) /\ w e. B ) ) -> ( v ( .r ` K ) w ) e. B )
7320oveqrspc2v 5994 . . . . . . . . . . . . 13 |- ( ( ph /\ ( ( u ( .r ` K ) w ) e. B /\ ( v ( .r ` K ) w ) e. B ) ) -> ( ( u ( .r ` K ) w ) ( +g ` K ) ( v ( .r ` K ) w ) ) = ( ( u ( .r ` K ) w ) ( +g ` L ) ( v ( .r ` K ) w ) ) )
741, 48, 72, 73syl12anc 1248 . . . . . . . . . . . 12 |- ( ( ( ph /\ ( K e. Abel /\ (mulGrp ` K ) e. Smgrp ) ) /\ ( ( u e. B /\ v e. B ) /\ w e. B ) ) -> ( ( u ( .r ` K ) w ) ( +g ` K ) ( v ( .r ` K ) w ) ) = ( ( u ( .r ` K ) w ) ( +g ` L ) ( v ( .r ` K ) w ) ) )
7517oveqrspc2v 5994 . . . . . . . . . . . . . 14 |- ( ( ph /\ ( v e. B /\ w e. B ) ) -> ( v ( .r ` K ) w ) = ( v ( .r ` L ) w ) )
761, 4, 8, 75syl12anc 1248 . . . . . . . . . . . . 13 |- ( ( ( ph /\ ( K e. Abel /\ (mulGrp ` K ) e. Smgrp ) ) /\ ( ( u e. B /\ v e. B ) /\ w e. B ) ) -> ( v ( .r ` K ) w ) = ( v ( .r ` L ) w ) )
7754, 76oveq12d 5985 . . . . . . . . . . . 12 |- ( ( ( ph /\ ( K e. Abel /\ (mulGrp ` K ) e. Smgrp ) ) /\ ( ( u e. B /\ v e. B ) /\ w e. B ) ) -> ( ( u ( .r ` K ) w ) ( +g ` L ) ( v ( .r ` K ) w ) ) = ( ( u ( .r ` L ) w ) ( +g ` L ) ( v ( .r ` L ) w ) ) )
7874, 77eqtrd 2240 . . . . . . . . . . 11 |- ( ( ( ph /\ ( K e. Abel /\ (mulGrp ` K ) e. Smgrp ) ) /\ ( ( u e. B /\ v e. B ) /\ w e. B ) ) -> ( ( u ( .r ` K ) w ) ( +g ` K ) ( v ( .r ` K ) w ) ) = ( ( u ( .r ` L ) w ) ( +g ` L ) ( v ( .r ` L ) w ) ) )
7967, 78eqeq12d 2222 . . . . . . . . . 10 |- ( ( ( ph /\ ( K e. Abel /\ (mulGrp ` K ) e. Smgrp ) ) /\ ( ( u e. B /\ v e. B ) /\ w e. B ) ) -> ( ( ( u ( +g ` K ) v ) ( .r ` K ) w ) = ( ( u ( .r ` K ) w ) ( +g ` K ) ( v ( .r ` K ) w ) ) <-> ( ( u ( +g ` L ) v ) ( .r ` L ) w ) = ( ( u ( .r ` L ) w ) ( +g ` L ) ( v ( .r ` L ) w ) ) ) )
8057, 79anbi12d 473 . . . . . . . . 9 |- ( ( ( ph /\ ( K e. Abel /\ (mulGrp ` K ) e. Smgrp ) ) /\ ( ( u e. B /\ v e. B ) /\ w e. B ) ) -> ( ( ( u ( .r ` K ) ( v ( +g ` K ) w ) ) = ( ( u ( .r ` K ) v ) ( +g ` K ) ( u ( .r ` K ) w ) ) /\ ( ( u ( +g ` K ) v ) ( .r ` K ) w ) = ( ( u ( .r ` K ) w ) ( +g ` K ) ( v ( .r ` K ) w ) ) ) <-> ( ( u ( .r ` L ) ( v ( +g ` L ) w ) ) = ( ( u ( .r ` L ) v ) ( +g ` L ) ( u ( .r ` L ) w ) ) /\ ( ( u ( +g ` L ) v ) ( .r ` L ) w ) = ( ( u ( .r ` L ) w ) ( +g ` L ) ( v ( .r ` L ) w ) ) ) ) )
8180anassrs 400 . . . . . . . 8 |- ( ( ( ( ph /\ ( K e. Abel /\ (mulGrp ` K ) e. Smgrp ) ) /\ ( u e. B /\ v e. B ) ) /\ w e. B ) -> ( ( ( u ( .r ` K ) ( v ( +g ` K ) w ) ) = ( ( u ( .r ` K ) v ) ( +g ` K ) ( u ( .r ` K ) w ) ) /\ ( ( u ( +g ` K ) v ) ( .r ` K ) w ) = ( ( u ( .r ` K ) w ) ( +g ` K ) ( v ( .r ` K ) w ) ) ) <-> ( ( u ( .r ` L ) ( v ( +g ` L ) w ) ) = ( ( u ( .r ` L ) v ) ( +g ` L ) ( u ( .r ` L ) w ) ) /\ ( ( u ( +g ` L ) v ) ( .r ` L ) w ) = ( ( u ( .r ` L ) w ) ( +g ` L ) ( v ( .r ` L ) w ) ) ) ) )
8281ralbidva 2504 . . . . . . 7 |- ( ( ( ph /\ ( K e. Abel /\ (mulGrp ` K ) e. Smgrp ) ) /\ ( u e. B /\ v e. B ) ) -> ( A. w e. B ( ( u ( .r ` K ) ( v ( +g ` K ) w ) ) = ( ( u ( .r ` K ) v ) ( +g ` K ) ( u ( .r ` K ) w ) ) /\ ( ( u ( +g ` K ) v ) ( .r ` K ) w ) = ( ( u ( .r ` K ) w ) ( +g ` K ) ( v ( .r ` K ) w ) ) ) <-> A. w e. B ( ( u ( .r ` L ) ( v ( +g ` L ) w ) ) = ( ( u ( .r ` L ) v ) ( +g ` L ) ( u ( .r ` L ) w ) ) /\ ( ( u ( +g ` L ) v ) ( .r ` L ) w ) = ( ( u ( .r ` L ) w ) ( +g ` L ) ( v ( .r ` L ) w ) ) ) ) )
83822ralbidva 2530 . . . . . 6 |- ( ( ph /\ ( K e. Abel /\ (mulGrp ` K ) e. Smgrp ) ) -> ( A. u e. B A. v e. B A. w e. B ( ( u ( .r ` K ) ( v ( +g ` K ) w ) ) = ( ( u ( .r ` K ) v ) ( +g ` K ) ( u ( .r ` K ) w ) ) /\ ( ( u ( +g ` K ) v ) ( .r ` K ) w ) = ( ( u ( .r ` K ) w ) ( +g ` K ) ( v ( .r ` K ) w ) ) ) <-> A. u e. B A. v e. B A. w e. B ( ( u ( .r ` L ) ( v ( +g ` L ) w ) ) = ( ( u ( .r ` L ) v ) ( +g ` L ) ( u ( .r ` L ) w ) ) /\ ( ( u ( +g ` L ) v ) ( .r ` L ) w ) = ( ( u ( .r ` L ) w ) ( +g ` L ) ( v ( .r ` L ) w ) ) ) ) )
845adantr 276 . . . . . . 7 |- ( ( ph /\ ( K e. Abel /\ (mulGrp ` K ) e. Smgrp ) ) -> B = ( Base ` K ) )
8584raleqdv 2711 . . . . . . . 8 |- ( ( ph /\ ( K e. Abel /\ (mulGrp ` K ) e. Smgrp ) ) -> ( A. w e. B ( ( u ( .r ` K ) ( v ( +g ` K ) w ) ) = ( ( u ( .r ` K ) v ) ( +g ` K ) ( u ( .r ` K ) w ) ) /\ ( ( u ( +g ` K ) v ) ( .r ` K ) w ) = ( ( u ( .r ` K ) w ) ( +g ` K ) ( v ( .r ` K ) w ) ) ) <-> A. w e. ( Base ` K ) ( ( u ( .r ` K ) ( v ( +g ` K ) w ) ) = ( ( u ( .r ` K ) v ) ( +g ` K ) ( u ( .r ` K ) w ) ) /\ ( ( u ( +g ` K ) v ) ( .r ` K ) w ) = ( ( u ( .r ` K ) w ) ( +g ` K ) ( v ( .r ` K ) w ) ) ) ) )
8684, 85raleqbidv 2721 . . . . . . 7 |- ( ( ph /\ ( K e. Abel /\ (mulGrp ` K ) e. Smgrp ) ) -> ( A. v e. B A. w e. B ( ( u ( .r ` K ) ( v ( +g ` K ) w ) ) = ( ( u ( .r ` K ) v ) ( +g ` K ) ( u ( .r ` K ) w ) ) /\ ( ( u ( +g ` K ) v ) ( .r ` K ) w ) = ( ( u ( .r ` K ) w ) ( +g ` K ) ( v ( .r ` K ) w ) ) ) <-> A. v e. ( Base ` K ) A. w e. ( Base ` K ) ( ( u ( .r ` K ) ( v ( +g ` K ) w ) ) = ( ( u ( .r ` K ) v ) ( +g ` K ) ( u ( .r ` K ) w ) ) /\ ( ( u ( +g ` K ) v ) ( .r ` K ) w ) = ( ( u ( .r ` K ) w ) ( +g ` K ) ( v ( .r ` K ) w ) ) ) ) )
8784, 86raleqbidv 2721 . . . . . 6 |- ( ( ph /\ ( K e. Abel /\ (mulGrp ` K ) e. Smgrp ) ) -> ( A. u e. B A. v e. B A. w e. B ( ( u ( .r ` K ) ( v ( +g ` K ) w ) ) = ( ( u ( .r ` K ) v ) ( +g ` K ) ( u ( .r ` K ) w ) ) /\ ( ( u ( +g ` K ) v ) ( .r ` K ) w ) = ( ( u ( .r ` K ) w ) ( +g ` K ) ( v ( .r ` K ) w ) ) ) <-> A. u e. ( Base ` K ) A. v e. ( Base ` K ) A. w e. ( Base ` K ) ( ( u ( .r ` K ) ( v ( +g ` K ) w ) ) = ( ( u ( .r ` K ) v ) ( +g ` K ) ( u ( .r ` K ) w ) ) /\ ( ( u ( +g ` K ) v ) ( .r ` K ) w ) = ( ( u ( .r ` K ) w ) ( +g ` K ) ( v ( .r ` K ) w ) ) ) ) )
88 rngpropd.2 . . . . . . . 8 |- ( ph -> B = ( Base ` L ) )
8988adantr 276 . . . . . . 7 |- ( ( ph /\ ( K e. Abel /\ (mulGrp ` K ) e. Smgrp ) ) -> B = ( Base ` L ) )
9089raleqdv 2711 . . . . . . . 8 |- ( ( ph /\ ( K e. Abel /\ (mulGrp ` K ) e. Smgrp ) ) -> ( A. w e. B ( ( u ( .r ` L ) ( v ( +g ` L ) w ) ) = ( ( u ( .r ` L ) v ) ( +g ` L ) ( u ( .r ` L ) w ) ) /\ ( ( u ( +g ` L ) v ) ( .r ` L ) w ) = ( ( u ( .r ` L ) w ) ( +g ` L ) ( v ( .r ` L ) w ) ) ) <-> A. w e. ( Base ` L ) ( ( u ( .r ` L ) ( v ( +g ` L ) w ) ) = ( ( u ( .r ` L ) v ) ( +g ` L ) ( u ( .r ` L ) w ) ) /\ ( ( u ( +g ` L ) v ) ( .r ` L ) w ) = ( ( u ( .r ` L ) w ) ( +g ` L ) ( v ( .r ` L ) w ) ) ) ) )
9189, 90raleqbidv 2721 . . . . . . 7 |- ( ( ph /\ ( K e. Abel /\ (mulGrp ` K ) e. Smgrp ) ) -> ( A. v e. B A. w e. B ( ( u ( .r ` L ) ( v ( +g ` L ) w ) ) = ( ( u ( .r ` L ) v ) ( +g ` L ) ( u ( .r ` L ) w ) ) /\ ( ( u ( +g ` L ) v ) ( .r ` L ) w ) = ( ( u ( .r ` L ) w ) ( +g ` L ) ( v ( .r ` L ) w ) ) ) <-> A. v e. ( Base ` L ) A. w e. ( Base ` L ) ( ( u ( .r ` L ) ( v ( +g ` L ) w ) ) = ( ( u ( .r ` L ) v ) ( +g ` L ) ( u ( .r ` L ) w ) ) /\ ( ( u ( +g ` L ) v ) ( .r ` L ) w ) = ( ( u ( .r ` L ) w ) ( +g ` L ) ( v ( .r ` L ) w ) ) ) ) )
9289, 91raleqbidv 2721 . . . . . 6 |- ( ( ph /\ ( K e. Abel /\ (mulGrp ` K ) e. Smgrp ) ) -> ( A. u e. B A. v e. B A. w e. B ( ( u ( .r ` L ) ( v ( +g ` L ) w ) ) = ( ( u ( .r ` L ) v ) ( +g ` L ) ( u ( .r ` L ) w ) ) /\ ( ( u ( +g ` L ) v ) ( .r ` L ) w ) = ( ( u ( .r ` L ) w ) ( +g ` L ) ( v ( .r ` L ) w ) ) ) <-> A. u e. ( Base ` L ) A. v e. ( Base ` L ) A. w e. ( Base ` L ) ( ( u ( .r ` L ) ( v ( +g ` L ) w ) ) = ( ( u ( .r ` L ) v ) ( +g ` L ) ( u ( .r ` L ) w ) ) /\ ( ( u ( +g ` L ) v ) ( .r ` L ) w ) = ( ( u ( .r ` L ) w ) ( +g ` L ) ( v ( .r ` L ) w ) ) ) ) )
9383, 87, 923bitr3d 218 . . . . 5 |- ( ( ph /\ ( K e. Abel /\ (mulGrp ` K ) e. Smgrp ) ) -> ( A. u e. ( Base ` K ) A. v e. ( Base ` K ) A. w e. ( Base ` K ) ( ( u ( .r ` K ) ( v ( +g ` K ) w ) ) = ( ( u ( .r ` K ) v ) ( +g ` K ) ( u ( .r ` K ) w ) ) /\ ( ( u ( +g ` K ) v ) ( .r ` K ) w ) = ( ( u ( .r ` K ) w ) ( +g ` K ) ( v ( .r ` K ) w ) ) ) <-> A. u e. ( Base ` L ) A. v e. ( Base ` L ) A. w e. ( Base ` L ) ( ( u ( .r ` L ) ( v ( +g ` L ) w ) ) = ( ( u ( .r ` L ) v ) ( +g ` L ) ( u ( .r ` L ) w ) ) /\ ( ( u ( +g ` L ) v ) ( .r ` L ) w ) = ( ( u ( .r ` L ) w ) ( +g ` L ) ( v ( .r ` L ) w ) ) ) ) )
9493pm5.32da 452 . . . 4 |- ( ph -> ( ( ( K e. Abel /\ (mulGrp ` K ) e. Smgrp ) /\ A. u e. ( Base ` K ) A. v e. ( Base ` K ) A. w e. ( Base ` K ) ( ( u ( .r ` K ) ( v ( +g ` K ) w ) ) = ( ( u ( .r ` K ) v ) ( +g ` K ) ( u ( .r ` K ) w ) ) /\ ( ( u ( +g ` K ) v ) ( .r ` K ) w ) = ( ( u ( .r ` K ) w ) ( +g ` K ) ( v ( .r ` K ) w ) ) ) ) <-> ( ( K e. Abel /\ (mulGrp ` K ) e. Smgrp ) /\ A. u e. ( Base ` L ) A. v e. ( Base ` L ) A. w e. ( Base ` L ) ( ( u ( .r ` L ) ( v ( +g ` L ) w ) ) = ( ( u ( .r ` L ) v ) ( +g ` L ) ( u ( .r ` L ) w ) ) /\ ( ( u ( +g ` L ) v ) ( .r ` L ) w ) = ( ( u ( .r ` L ) w ) ( +g ` L ) ( v ( .r ` L ) w ) ) ) ) ) )
95 df-3an 983 . . . 4 |- ( ( K e. Abel /\ (mulGrp ` K ) e. Smgrp /\ A. u e. ( Base ` K ) A. v e. ( Base ` K ) A. w e. ( Base ` K ) ( ( u ( .r ` K ) ( v ( +g ` K ) w ) ) = ( ( u ( .r ` K ) v ) ( +g ` K ) ( u ( .r ` K ) w ) ) /\ ( ( u ( +g ` K ) v ) ( .r ` K ) w ) = ( ( u ( .r ` K ) w ) ( +g ` K ) ( v ( .r ` K ) w ) ) ) ) <-> ( ( K e. Abel /\ (mulGrp ` K ) e. Smgrp ) /\ A. u e. ( Base ` K ) A. v e. ( Base ` K ) A. w e. ( Base ` K ) ( ( u ( .r ` K ) ( v ( +g ` K ) w ) ) = ( ( u ( .r ` K ) v ) ( +g ` K ) ( u ( .r ` K ) w ) ) /\ ( ( u ( +g ` K ) v ) ( .r ` K ) w ) = ( ( u ( .r ` K ) w ) ( +g ` K ) ( v ( .r ` K ) w ) ) ) ) )
96 df-3an 983 . . . 4 |- ( ( K e. Abel /\ (mulGrp ` K ) e. Smgrp /\ A. u e. ( Base ` L ) A. v e. ( Base ` L ) A. w e. ( Base ` L ) ( ( u ( .r ` L ) ( v ( +g ` L ) w ) ) = ( ( u ( .r ` L ) v ) ( +g ` L ) ( u ( .r ` L ) w ) ) /\ ( ( u ( +g ` L ) v ) ( .r ` L ) w ) = ( ( u ( .r ` L ) w ) ( +g ` L ) ( v ( .r ` L ) w ) ) ) ) <-> ( ( K e. Abel /\ (mulGrp ` K ) e. Smgrp ) /\ A. u e. ( Base ` L ) A. v e. ( Base ` L ) A. w e. ( Base ` L ) ( ( u ( .r ` L ) ( v ( +g ` L ) w ) ) = ( ( u ( .r ` L ) v ) ( +g ` L ) ( u ( .r ` L ) w ) ) /\ ( ( u ( +g ` L ) v ) ( .r ` L ) w ) = ( ( u ( .r ` L ) w ) ( +g ` L ) ( v ( .r ` L ) w ) ) ) ) )
9794, 95, 963bitr4g 223 . . 3 |- ( ph -> ( ( K e. Abel /\ (mulGrp ` K ) e. Smgrp /\ A. u e. ( Base ` K ) A. v e. ( Base ` K ) A. w e. ( Base ` K ) ( ( u ( .r ` K ) ( v ( +g ` K ) w ) ) = ( ( u ( .r ` K ) v ) ( +g ` K ) ( u ( .r ` K ) w ) ) /\ ( ( u ( +g ` K ) v ) ( .r ` K ) w ) = ( ( u ( .r ` K ) w ) ( +g ` K ) ( v ( .r ` K ) w ) ) ) ) <-> ( K e. Abel /\ (mulGrp ` K ) e. Smgrp /\ A. u e. ( Base ` L ) A. v e. ( Base ` L ) A. w e. ( Base ` L ) ( ( u ( .r ` L ) ( v ( +g ` L ) w ) ) = ( ( u ( .r ` L ) v ) ( +g ` L ) ( u ( .r ` L ) w ) ) /\ ( ( u ( +g ` L ) v ) ( .r ` L ) w ) = ( ( u ( .r ` L ) w ) ( +g ` L ) ( v ( .r ` L ) w ) ) ) ) ) )
98 simp1 1000 . . . . 5 |- ( ( K e. Abel /\ (mulGrp ` K ) e. Smgrp /\ A. u e. ( Base ` L ) A. v e. ( Base ` L ) A. w e. ( Base ` L ) ( ( u ( .r ` L ) ( v ( +g ` L ) w ) ) = ( ( u ( .r ` L ) v ) ( +g ` L ) ( u ( .r ` L ) w ) ) /\ ( ( u ( +g ` L ) v ) ( .r ` L ) w ) = ( ( u ( .r ` L ) w ) ( +g ` L ) ( v ( .r ` L ) w ) ) ) ) -> K e. Abel )
9998a1i 9 . . . 4 |- ( ph -> ( ( K e. Abel /\ (mulGrp ` K ) e. Smgrp /\ A. u e. ( Base ` L ) A. v e. ( Base ` L ) A. w e. ( Base ` L ) ( ( u ( .r ` L ) ( v ( +g ` L ) w ) ) = ( ( u ( .r ` L ) v ) ( +g ` L ) ( u ( .r ` L ) w ) ) /\ ( ( u ( +g ` L ) v ) ( .r ` L ) w ) = ( ( u ( .r ` L ) w ) ( +g ` L ) ( v ( .r ` L ) w ) ) ) ) -> K e. Abel ) )
100 simp1 1000 . . . . 5 |- ( ( L e. Abel /\ (mulGrp ` L ) e. Smgrp /\ A. u e. ( Base ` L ) A. v e. ( Base ` L ) A. w e. ( Base ` L ) ( ( u ( .r ` L ) ( v ( +g ` L ) w ) ) = ( ( u ( .r ` L ) v ) ( +g ` L ) ( u ( .r ` L ) w ) ) /\ ( ( u ( +g ` L ) v ) ( .r ` L ) w ) = ( ( u ( .r ` L ) w ) ( +g ` L ) ( v ( .r ` L ) w ) ) ) ) -> L e. Abel )
1015, 88, 20ablpropd 13747 . . . . 5 |- ( ph -> ( K e. Abel <-> L e. Abel ) )
102100, 101imbitrrid 156 . . . 4 |- ( ph -> ( ( L e. Abel /\ (mulGrp ` L ) e. Smgrp /\ A. u e. ( Base ` L ) A. v e. ( Base ` L ) A. w e. ( Base ` L ) ( ( u ( .r ` L ) ( v ( +g ` L ) w ) ) = ( ( u ( .r ` L ) v ) ( +g ` L ) ( u ( .r ` L ) w ) ) /\ ( ( u ( +g ` L ) v ) ( .r ` L ) w ) = ( ( u ( .r ` L ) w ) ( +g ` L ) ( v ( .r ` L ) w ) ) ) ) -> K e. Abel ) )
103101adantr 276 . . . . . 6 |- ( ( ph /\ K e. Abel ) -> ( K e. Abel <-> L e. Abel ) )
10428mgpex 13802 . . . . . . . 8 |- ( K e. Abel -> (mulGrp ` K ) e. _V )
105104adantl 277 . . . . . . 7 |- ( ( ph /\ K e. Abel ) -> (mulGrp ` K ) e. _V )
106101biimpa 296 . . . . . . . 8 |- ( ( ph /\ K e. Abel ) -> L e. Abel )
107 eqid 2207 . . . . . . . . 9 |- (mulGrp ` L ) = (mulGrp ` L )
108107mgpex 13802 . . . . . . . 8 |- ( L e. Abel -> (mulGrp ` L ) e. _V )
109106, 108syl 14 . . . . . . 7 |- ( ( ph /\ K e. Abel ) -> (mulGrp ` L ) e. _V )
110 elex 2788 . . . . . . . . 9 |- ( K e. Abel -> K e. _V )
111110adantl 277 . . . . . . . 8 |- ( ( ph /\ K e. Abel ) -> K e. _V )
112111, 29syl 14 . . . . . . 7 |- ( ( ph /\ K e. Abel ) -> ( Base ` K ) = ( Base ` (mulGrp ` K ) ) )
1135eqcomd 2213 . . . . . . . . 9 |- ( ph -> ( Base ` K ) = B )
114113adantr 276 . . . . . . . 8 |- ( ( ph /\ K e. Abel ) -> ( Base ` K ) = B )
11588adantr 276 . . . . . . . . 9 |- ( ( ph /\ K e. Abel ) -> B = ( Base ` L ) )
116 eqid 2207 . . . . . . . . . . 11 |- ( Base ` L ) = ( Base ` L )
117107, 116mgpbasg 13803 . . . . . . . . . 10 |- ( L e. Abel -> ( Base ` L ) = ( Base ` (mulGrp ` L ) ) )
118106, 117syl 14 . . . . . . . . 9 |- ( ( ph /\ K e. Abel ) -> ( Base ` L ) = ( Base ` (mulGrp ` L ) ) )
119115, 118eqtrd 2240 . . . . . . . 8 |- ( ( ph /\ K e. Abel ) -> B = ( Base ` (mulGrp ` L ) ) )
120114, 119eqtrd 2240 . . . . . . 7 |- ( ( ph /\ K e. Abel ) -> ( Base ` K ) = ( Base ` (mulGrp ` L ) ) )
12117ex 115 . . . . . . . . . 10 |- ( ph -> ( ( x e. B /\ y e. B ) -> ( x ( .r ` K ) y ) = ( x ( .r ` L ) y ) ) )
122121adantr 276 . . . . . . . . 9 |- ( ( ph /\ K e. Abel ) -> ( ( x e. B /\ y e. B ) -> ( x ( .r ` K ) y ) = ( x ( .r ` L ) y ) ) )
1235eleq2d 2277 . . . . . . . . . . . 12 |- ( ph -> ( x e. B <-> x e. ( Base ` K ) ) )
1245eleq2d 2277 . . . . . . . . . . . 12 |- ( ph -> ( y e. B <-> y e. ( Base ` K ) ) )
125123, 124anbi12d 473 . . . . . . . . . . 11 |- ( ph -> ( ( x e. B /\ y e. B ) <-> ( x e. ( Base ` K ) /\ y e. ( Base ` K ) ) ) )
126125bicomd 141 . . . . . . . . . 10 |- ( ph -> ( ( x e. ( Base ` K ) /\ y e. ( Base ` K ) ) <-> ( x e. B /\ y e. B ) ) )
127126adantr 276 . . . . . . . . 9 |- ( ( ph /\ K e. Abel ) -> ( ( x e. ( Base ` K ) /\ y e. ( Base ` K ) ) <-> ( x e. B /\ y e. B ) ) )
128111, 38syl 14 . . . . . . . . . . . 12 |- ( ( ph /\ K e. Abel ) -> ( .r ` K ) = ( +g ` (mulGrp ` K ) ) )
129128eqcomd 2213 . . . . . . . . . . 11 |- ( ( ph /\ K e. Abel ) -> ( +g ` (mulGrp ` K ) ) = ( .r ` K ) )
130129oveqd 5984 . . . . . . . . . 10 |- ( ( ph /\ K e. Abel ) -> ( x ( +g ` (mulGrp ` K ) ) y ) = ( x ( .r ` K ) y ) )
131 eqid 2207 . . . . . . . . . . . . . 14 |- ( .r ` L ) = ( .r ` L )
132107, 131mgpplusgg 13801 . . . . . . . . . . . . 13 |- ( L e. Abel -> ( .r ` L ) = ( +g ` (mulGrp ` L ) ) )
133106, 132syl 14 . . . . . . . . . . . 12 |- ( ( ph /\ K e. Abel ) -> ( .r ` L ) = ( +g ` (mulGrp ` L ) ) )
134133eqcomd 2213 . . . . . . . . . . 11 |- ( ( ph /\ K e. Abel ) -> ( +g ` (mulGrp ` L ) ) = ( .r ` L ) )
135134oveqd 5984 . . . . . . . . . 10 |- ( ( ph /\ K e. Abel ) -> ( x ( +g ` (mulGrp ` L ) ) y ) = ( x ( .r ` L ) y ) )
136130, 135eqeq12d 2222 . . . . . . . . 9 |- ( ( ph /\ K e. Abel ) -> ( ( x ( +g ` (mulGrp ` K ) ) y ) = ( x ( +g ` (mulGrp ` L ) ) y ) <-> ( x ( .r ` K ) y ) = ( x ( .r ` L ) y ) ) )
137122, 127, 1363imtr4d 203 . . . . . . . 8 |- ( ( ph /\ K e. Abel ) -> ( ( x e. ( Base ` K ) /\ y e. ( Base ` K ) ) -> ( x ( +g ` (mulGrp ` K ) ) y ) = ( x ( +g ` (mulGrp ` L ) ) y ) ) )
138137imp 124 . . . . . . 7 |- ( ( ( ph /\ K e. Abel ) /\ ( x e. ( Base ` K ) /\ y e. ( Base ` K ) ) ) -> ( x ( +g ` (mulGrp ` K ) ) y ) = ( x ( +g ` (mulGrp ` L ) ) y ) )
139105, 109, 112, 120, 138sgrppropd 13360 . . . . . 6 |- ( ( ph /\ K e. Abel ) -> ( (mulGrp ` K ) e. Smgrp <-> (mulGrp ` L ) e. Smgrp ) )
140103, 1393anbi12d 1326 . . . . 5 |- ( ( ph /\ K e. Abel ) -> ( ( K e. Abel /\ (mulGrp ` K ) e. Smgrp /\ A. u e. ( Base ` L ) A. v e. ( Base ` L ) A. w e. ( Base ` L ) ( ( u ( .r ` L ) ( v ( +g ` L ) w ) ) = ( ( u ( .r ` L ) v ) ( +g ` L ) ( u ( .r ` L ) w ) ) /\ ( ( u ( +g ` L ) v ) ( .r ` L ) w ) = ( ( u ( .r ` L ) w ) ( +g ` L ) ( v ( .r ` L ) w ) ) ) ) <-> ( L e. Abel /\ (mulGrp ` L ) e. Smgrp /\ A. u e. ( Base ` L ) A. v e. ( Base ` L ) A. w e. ( Base ` L ) ( ( u ( .r ` L ) ( v ( +g ` L ) w ) ) = ( ( u ( .r ` L ) v ) ( +g ` L ) ( u ( .r ` L ) w ) ) /\ ( ( u ( +g ` L ) v ) ( .r ` L ) w ) = ( ( u ( .r ` L ) w ) ( +g ` L ) ( v ( .r ` L ) w ) ) ) ) ) )
141140ex 115 . . . 4 |- ( ph -> ( K e. Abel -> ( ( K e. Abel /\ (mulGrp ` K ) e. Smgrp /\ A. u e. ( Base ` L ) A. v e. ( Base ` L ) A. w e. ( Base ` L ) ( ( u ( .r ` L ) ( v ( +g ` L ) w ) ) = ( ( u ( .r ` L ) v ) ( +g ` L ) ( u ( .r ` L ) w ) ) /\ ( ( u ( +g ` L ) v ) ( .r ` L ) w ) = ( ( u ( .r ` L ) w ) ( +g ` L ) ( v ( .r ` L ) w ) ) ) ) <-> ( L e. Abel /\ (mulGrp ` L ) e. Smgrp /\ A. u e. ( Base ` L ) A. v e. ( Base ` L ) A. w e. ( Base ` L ) ( ( u ( .r ` L ) ( v ( +g ` L ) w ) ) = ( ( u ( .r ` L ) v ) ( +g ` L ) ( u ( .r ` L ) w ) ) /\ ( ( u ( +g ` L ) v ) ( .r ` L ) w ) = ( ( u ( .r ` L ) w ) ( +g ` L ) ( v ( .r ` L ) w ) ) ) ) ) ) )
14299, 102, 141pm5.21ndd 707 . . 3 |- ( ph -> ( ( K e. Abel /\ (mulGrp ` K ) e. Smgrp /\ A. u e. ( Base ` L ) A. v e. ( Base ` L ) A. w e. ( Base ` L ) ( ( u ( .r ` L ) ( v ( +g ` L ) w ) ) = ( ( u ( .r ` L ) v ) ( +g ` L ) ( u ( .r ` L ) w ) ) /\ ( ( u ( +g ` L ) v ) ( .r ` L ) w ) = ( ( u ( .r ` L ) w ) ( +g ` L ) ( v ( .r ` L ) w ) ) ) ) <-> ( L e. Abel /\ (mulGrp ` L ) e. Smgrp /\ A. u e. ( Base ` L ) A. v e. ( Base ` L ) A. w e. ( Base ` L ) ( ( u ( .r ` L ) ( v ( +g ` L ) w ) ) = ( ( u ( .r ` L ) v ) ( +g ` L ) ( u ( .r ` L ) w ) ) /\ ( ( u ( +g ` L ) v ) ( .r ` L ) w ) = ( ( u ( .r ` L ) w ) ( +g ` L ) ( v ( .r ` L ) w ) ) ) ) ) )
14397, 142bitrd 188 . 2 |- ( ph -> ( ( K e. Abel /\ (mulGrp ` K ) e. Smgrp /\ A. u e. ( Base ` K ) A. v e. ( Base ` K ) A. w e. ( Base ` K ) ( ( u ( .r ` K ) ( v ( +g ` K ) w ) ) = ( ( u ( .r ` K ) v ) ( +g ` K ) ( u ( .r ` K ) w ) ) /\ ( ( u ( +g ` K ) v ) ( .r ` K ) w ) = ( ( u ( .r ` K ) w ) ( +g ` K ) ( v ( .r ` K ) w ) ) ) ) <-> ( L e. Abel /\ (mulGrp ` L ) e. Smgrp /\ A. u e. ( Base ` L ) A. v e. ( Base ` L ) A. w e. ( Base ` L ) ( ( u ( .r ` L ) ( v ( +g ` L ) w ) ) = ( ( u ( .r ` L ) v ) ( +g ` L ) ( u ( .r ` L ) w ) ) /\ ( ( u ( +g ` L ) v ) ( .r ` L ) w ) = ( ( u ( .r ` L ) w ) ( +g ` L ) ( v ( .r ` L ) w ) ) ) ) ) )
14411, 28, 12, 37isrng 13811 . 2 |- ( K e. Rng <-> ( K e. Abel /\ (mulGrp ` K ) e. Smgrp /\ A. u e. ( Base ` K ) A. v e. ( Base ` K ) A. w e. ( Base ` K ) ( ( u ( .r ` K ) ( v ( +g ` K ) w ) ) = ( ( u ( .r ` K ) v ) ( +g ` K ) ( u ( .r ` K ) w ) ) /\ ( ( u ( +g ` K ) v ) ( .r ` K ) w ) = ( ( u ( .r ` K ) w ) ( +g ` K ) ( v ( .r ` K ) w ) ) ) ) )
145 eqid 2207 . . 3 |- ( +g ` L ) = ( +g ` L )
146116, 107, 145, 131isrng 13811 . 2 |- ( L e. Rng <-> ( L e. Abel /\ (mulGrp ` L ) e. Smgrp /\ A. u e. ( Base ` L ) A. v e. ( Base ` L ) A. w e. ( Base ` L ) ( ( u ( .r ` L ) ( v ( +g ` L ) w ) ) = ( ( u ( .r ` L ) v ) ( +g ` L ) ( u ( .r ` L ) w ) ) /\ ( ( u ( +g ` L ) v ) ( .r ` L ) w ) = ( ( u ( .r ` L ) w ) ( +g ` L ) ( v ( .r ` L ) w ) ) ) ) )
147143, 144, 1463bitr4g 223 1 |- ( ph -> ( K e. Rng <-> L e. Rng ) )
Colors of variables: wff set class
Syntax hints:   -> wi 4   /\ wa 104   <-> wb 105   /\ w3a 981   = wceq 1373   e. wcel 2178   A.wral 2486   _Vcvv 2776   ` cfv 5290  (class class class)co 5967   Basecbs 12947   +g cplusg 13024   .rcmulr 13025  Smgrpcsgrp 13348   Grpcgrp 13447   Abelcabl 13736  mulGrpcmgp 13797  Rngcrng 13809
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 615  ax-in2 616  ax-io 711  ax-5 1471  ax-7 1472  ax-gen 1473  ax-ie1 1517  ax-ie2 1518  ax-8 1528  ax-10 1529  ax-11 1530  ax-i12 1531  ax-bndl 1533  ax-4 1534  ax-17 1550  ax-i9 1554  ax-ial 1558  ax-i5r 1559  ax-13 2180  ax-14 2181  ax-ext 2189  ax-sep 4178  ax-pow 4234  ax-pr 4269  ax-un 4498  ax-setind 4603  ax-cnex 8051  ax-resscn 8052  ax-1cn 8053  ax-1re 8054  ax-icn 8055  ax-addcl 8056  ax-addrcl 8057  ax-mulcl 8058  ax-addcom 8060  ax-addass 8062  ax-i2m1 8065  ax-0lt1 8066  ax-0id 8068  ax-rnegex 8069  ax-pre-ltirr 8072  ax-pre-ltadd 8076
This theorem depends on definitions:  df-bi 117  df-3an 983  df-tru 1376  df-fal 1379  df-nf 1485  df-sb 1787  df-eu 2058  df-mo 2059  df-clab 2194  df-cleq 2200  df-clel 2203  df-nfc 2339  df-ne 2379  df-nel 2474  df-ral 2491  df-rex 2492  df-rab 2495  df-v 2778  df-sbc 3006  df-csb 3102  df-dif 3176  df-un 3178  df-in 3180  df-ss 3187  df-nul 3469  df-pw 3628  df-sn 3649  df-pr 3650  df-op 3652  df-uni 3865  df-int 3900  df-br 4060  df-opab 4122  df-mpt 4123  df-id 4358  df-xp 4699  df-rel 4700  df-cnv 4701  df-co 4702  df-dm 4703  df-rn 4704  df-res 4705  df-iota 5251  df-fun 5292  df-fn 5293  df-fv 5298  df-riota 5922  df-ov 5970  df-oprab 5971  df-mpo 5972  df-pnf 8144  df-mnf 8145  df-ltxr 8147  df-inn 9072  df-2 9130  df-3 9131  df-ndx 12950  df-slot 12951  df-base 12953  df-sets 12954  df-plusg 13037  df-mulr 13038  df-0g 13205  df-mgm 13303  df-sgrp 13349  df-mnd 13364  df-grp 13450  df-cmn 13737  df-abl 13738  df-mgp 13798  df-rng 13810
This theorem is referenced by:  opprrngbg  13955  subrngpropd  14093
  Copyright terms: Public domain W3C validator