Metamath Proof Explorer

Theorem lmodprop2d

Description: If two structures have the same components (properties), one is a left module iff the other one is. This version of lmodpropd also breaks up the components of the scalar ring. (Contributed by Mario Carneiro, 27-Jun-2015)

Ref Expression
Hypotheses lmodprop2d.b1 
|- ( ph -> B = ( Base ` K ) )
lmodprop2d.b2 
|- ( ph -> B = ( Base ` L ) )
lmodprop2d.f 
|- F = ( Scalar ` K )
lmodprop2d.g 
|- G = ( Scalar ` L )
lmodprop2d.p1 
|- ( ph -> P = ( Base ` F ) )
lmodprop2d.p2 
|- ( ph -> P = ( Base ` G ) )
lmodprop2d.1 
|- ( ( ph /\ ( x e. B /\ y e. B ) ) -> ( x ( +g ` K ) y ) = ( x ( +g ` L ) y ) )
lmodprop2d.2 
|- ( ( ph /\ ( x e. P /\ y e. P ) ) -> ( x ( +g ` F ) y ) = ( x ( +g ` G ) y ) )
lmodprop2d.3 
|- ( ( ph /\ ( x e. P /\ y e. P ) ) -> ( x ( .r ` F ) y ) = ( x ( .r ` G ) y ) )
lmodprop2d.4 
|- ( ( ph /\ ( x e. P /\ y e. B ) ) -> ( x ( .s ` K ) y ) = ( x ( .s ` L ) y ) )
Assertion lmodprop2d 
|- ( ph -> ( K e. LMod <-> L e. LMod ) )

Proof

Step Hyp Ref Expression
1 lmodprop2d.b1 
 |-  ( ph -> B = ( Base ` K ) )
2 lmodprop2d.b2 
 |-  ( ph -> B = ( Base ` L ) )
3 lmodprop2d.f 
 |-  F = ( Scalar ` K )
4 lmodprop2d.g 
 |-  G = ( Scalar ` L )
5 lmodprop2d.p1 
 |-  ( ph -> P = ( Base ` F ) )
6 lmodprop2d.p2 
 |-  ( ph -> P = ( Base ` G ) )
7 lmodprop2d.1 
 |-  ( ( ph /\ ( x e. B /\ y e. B ) ) -> ( x ( +g ` K ) y ) = ( x ( +g ` L ) y ) )
8 lmodprop2d.2 
 |-  ( ( ph /\ ( x e. P /\ y e. P ) ) -> ( x ( +g ` F ) y ) = ( x ( +g ` G ) y ) )
9 lmodprop2d.3 
 |-  ( ( ph /\ ( x e. P /\ y e. P ) ) -> ( x ( .r ` F ) y ) = ( x ( .r ` G ) y ) )
10 lmodprop2d.4 
 |-  ( ( ph /\ ( x e. P /\ y e. B ) ) -> ( x ( .s ` K ) y ) = ( x ( .s ` L ) y ) )
11 lmodgrp 
 |-  ( K e. LMod -> K e. Grp )
12 11 a1i 
 |-  ( ph -> ( K e. LMod -> K e. Grp ) )
13 eqid 
 |-  ( Base ` K ) = ( Base ` K )
14 eqid 
 |-  ( +g ` K ) = ( +g ` K )
15 eqid 
 |-  ( .s ` K ) = ( .s ` K )
16 eqid 
 |-  ( Base ` F ) = ( Base ` F )
17 eqid 
 |-  ( +g ` F ) = ( +g ` F )
18 eqid 
 |-  ( .r ` F ) = ( .r ` F )
19 eqid 
 |-  ( 1r ` F ) = ( 1r ` F )
20 13 14 15 3 16 17 18 19 islmod 
 |-  ( K e. LMod <-> ( K e. Grp /\ F e. Ring /\ A. q e. ( Base ` F ) A. r e. ( Base ` F ) A. z e. ( Base ` K ) A. w e. ( Base ` K ) ( ( ( r ( .s ` K ) w ) e. ( Base ` K ) /\ ( r ( .s ` K ) ( w ( +g ` K ) z ) ) = ( ( r ( .s ` K ) w ) ( +g ` K ) ( r ( .s ` K ) z ) ) /\ ( ( q ( +g ` F ) r ) ( .s ` K ) w ) = ( ( q ( .s ` K ) w ) ( +g ` K ) ( r ( .s ` K ) w ) ) ) /\ ( ( ( q ( .r ` F ) r ) ( .s ` K ) w ) = ( q ( .s ` K ) ( r ( .s ` K ) w ) ) /\ ( ( 1r ` F ) ( .s ` K ) w ) = w ) ) ) )
21 20 simp2bi 
 |-  ( K e. LMod -> F e. Ring )
22 21 a1i 
 |-  ( ph -> ( K e. LMod -> F e. Ring ) )
23 simplr 
 |-  ( ( ( ph /\ K e. LMod ) /\ ( x e. P /\ y e. B ) ) -> K e. LMod )
24 simprl 
 |-  ( ( ( ph /\ K e. LMod ) /\ ( x e. P /\ y e. B ) ) -> x e. P )
25 5 ad2antrr 
 |-  ( ( ( ph /\ K e. LMod ) /\ ( x e. P /\ y e. B ) ) -> P = ( Base ` F ) )
26 24 25 eleqtrd 
 |-  ( ( ( ph /\ K e. LMod ) /\ ( x e. P /\ y e. B ) ) -> x e. ( Base ` F ) )
27 simprr 
 |-  ( ( ( ph /\ K e. LMod ) /\ ( x e. P /\ y e. B ) ) -> y e. B )
28 1 ad2antrr 
 |-  ( ( ( ph /\ K e. LMod ) /\ ( x e. P /\ y e. B ) ) -> B = ( Base ` K ) )
29 27 28 eleqtrd 
 |-  ( ( ( ph /\ K e. LMod ) /\ ( x e. P /\ y e. B ) ) -> y e. ( Base ` K ) )
30 13 3 15 16 lmodvscl 
 |-  ( ( K e. LMod /\ x e. ( Base ` F ) /\ y e. ( Base ` K ) ) -> ( x ( .s ` K ) y ) e. ( Base ` K ) )
31 23 26 29 30 syl3anc 
 |-  ( ( ( ph /\ K e. LMod ) /\ ( x e. P /\ y e. B ) ) -> ( x ( .s ` K ) y ) e. ( Base ` K ) )
32 31 28 eleqtrrd 
 |-  ( ( ( ph /\ K e. LMod ) /\ ( x e. P /\ y e. B ) ) -> ( x ( .s ` K ) y ) e. B )
33 32 ralrimivva 
 |-  ( ( ph /\ K e. LMod ) -> A. x e. P A. y e. B ( x ( .s ` K ) y ) e. B )
34 33 ex 
 |-  ( ph -> ( K e. LMod -> A. x e. P A. y e. B ( x ( .s ` K ) y ) e. B ) )
35 12 22 34 3jcad 
 |-  ( ph -> ( K e. LMod -> ( K e. Grp /\ F e. Ring /\ A. x e. P A. y e. B ( x ( .s ` K ) y ) e. B ) ) )
36 lmodgrp 
 |-  ( L e. LMod -> L e. Grp )
37 1 2 7 grppropd 
 |-  ( ph -> ( K e. Grp <-> L e. Grp ) )
38 36 37 imbitrrid 
 |-  ( ph -> ( L e. LMod -> K e. Grp ) )
39 eqid 
 |-  ( Base ` L ) = ( Base ` L )
40 eqid 
 |-  ( +g ` L ) = ( +g ` L )
41 eqid 
 |-  ( .s ` L ) = ( .s ` L )
42 eqid 
 |-  ( Base ` G ) = ( Base ` G )
43 eqid 
 |-  ( +g ` G ) = ( +g ` G )
44 eqid 
 |-  ( .r ` G ) = ( .r ` G )
45 eqid 
 |-  ( 1r ` G ) = ( 1r ` G )
46 39 40 41 4 42 43 44 45 islmod 
 |-  ( L e. LMod <-> ( L e. Grp /\ G e. Ring /\ A. q e. ( Base ` G ) A. r e. ( Base ` G ) A. z e. ( Base ` L ) A. w e. ( Base ` L ) ( ( ( r ( .s ` L ) w ) e. ( Base ` L ) /\ ( r ( .s ` L ) ( w ( +g ` L ) z ) ) = ( ( r ( .s ` L ) w ) ( +g ` L ) ( r ( .s ` L ) z ) ) /\ ( ( q ( +g ` G ) r ) ( .s ` L ) w ) = ( ( q ( .s ` L ) w ) ( +g ` L ) ( r ( .s ` L ) w ) ) ) /\ ( ( ( q ( .r ` G ) r ) ( .s ` L ) w ) = ( q ( .s ` L ) ( r ( .s ` L ) w ) ) /\ ( ( 1r ` G ) ( .s ` L ) w ) = w ) ) ) )
47 46 simp2bi 
 |-  ( L e. LMod -> G e. Ring )
48 5 6 8 9 ringpropd 
 |-  ( ph -> ( F e. Ring <-> G e. Ring ) )
49 47 48 imbitrrid 
 |-  ( ph -> ( L e. LMod -> F e. Ring ) )
50 simplr 
 |-  ( ( ( ph /\ L e. LMod ) /\ ( x e. P /\ y e. B ) ) -> L e. LMod )
51 simprl 
 |-  ( ( ( ph /\ L e. LMod ) /\ ( x e. P /\ y e. B ) ) -> x e. P )
52 6 ad2antrr 
 |-  ( ( ( ph /\ L e. LMod ) /\ ( x e. P /\ y e. B ) ) -> P = ( Base ` G ) )
53 51 52 eleqtrd 
 |-  ( ( ( ph /\ L e. LMod ) /\ ( x e. P /\ y e. B ) ) -> x e. ( Base ` G ) )
54 simprr 
 |-  ( ( ( ph /\ L e. LMod ) /\ ( x e. P /\ y e. B ) ) -> y e. B )
55 2 ad2antrr 
 |-  ( ( ( ph /\ L e. LMod ) /\ ( x e. P /\ y e. B ) ) -> B = ( Base ` L ) )
56 54 55 eleqtrd 
 |-  ( ( ( ph /\ L e. LMod ) /\ ( x e. P /\ y e. B ) ) -> y e. ( Base ` L ) )
57 39 4 41 42 lmodvscl 
 |-  ( ( L e. LMod /\ x e. ( Base ` G ) /\ y e. ( Base ` L ) ) -> ( x ( .s ` L ) y ) e. ( Base ` L ) )
58 50 53 56 57 syl3anc 
 |-  ( ( ( ph /\ L e. LMod ) /\ ( x e. P /\ y e. B ) ) -> ( x ( .s ` L ) y ) e. ( Base ` L ) )
59 10 adantlr 
 |-  ( ( ( ph /\ L e. LMod ) /\ ( x e. P /\ y e. B ) ) -> ( x ( .s ` K ) y ) = ( x ( .s ` L ) y ) )
60 58 59 55 3eltr4d 
 |-  ( ( ( ph /\ L e. LMod ) /\ ( x e. P /\ y e. B ) ) -> ( x ( .s ` K ) y ) e. B )
61 60 ralrimivva 
 |-  ( ( ph /\ L e. LMod ) -> A. x e. P A. y e. B ( x ( .s ` K ) y ) e. B )
62 61 ex 
 |-  ( ph -> ( L e. LMod -> A. x e. P A. y e. B ( x ( .s ` K ) y ) e. B ) )
63 38 49 62 3jcad 
 |-  ( ph -> ( L e. LMod -> ( K e. Grp /\ F e. Ring /\ A. x e. P A. y e. B ( x ( .s ` K ) y ) e. B ) ) )
64 37 adantr 
 |-  ( ( ph /\ ( K e. Grp /\ F e. Ring /\ A. x e. P A. y e. B ( x ( .s ` K ) y ) e. B ) ) -> ( K e. Grp <-> L e. Grp ) )
65 48 adantr 
 |-  ( ( ph /\ ( K e. Grp /\ F e. Ring /\ A. x e. P A. y e. B ( x ( .s ` K ) y ) e. B ) ) -> ( F e. Ring <-> G e. Ring ) )
66 simpll 
 |-  ( ( ( ph /\ ( K e. Grp /\ F e. Ring /\ A. x e. P A. y e. B ( x ( .s ` K ) y ) e. B ) ) /\ ( ( q e. P /\ r e. P ) /\ ( z e. B /\ w e. B ) ) ) -> ph )
67 simprlr 
 |-  ( ( ( ph /\ ( K e. Grp /\ F e. Ring /\ A. x e. P A. y e. B ( x ( .s ` K ) y ) e. B ) ) /\ ( ( q e. P /\ r e. P ) /\ ( z e. B /\ w e. B ) ) ) -> r e. P )
68 simprrr 
 |-  ( ( ( ph /\ ( K e. Grp /\ F e. Ring /\ A. x e. P A. y e. B ( x ( .s ` K ) y ) e. B ) ) /\ ( ( q e. P /\ r e. P ) /\ ( z e. B /\ w e. B ) ) ) -> w e. B )
69 10 oveqrspc2v 
 |-  ( ( ph /\ ( r e. P /\ w e. B ) ) -> ( r ( .s ` K ) w ) = ( r ( .s ` L ) w ) )
70 66 67 68 69 syl12anc 
 |-  ( ( ( ph /\ ( K e. Grp /\ F e. Ring /\ A. x e. P A. y e. B ( x ( .s ` K ) y ) e. B ) ) /\ ( ( q e. P /\ r e. P ) /\ ( z e. B /\ w e. B ) ) ) -> ( r ( .s ` K ) w ) = ( r ( .s ` L ) w ) )
71 70 eleq1d 
 |-  ( ( ( ph /\ ( K e. Grp /\ F e. Ring /\ A. x e. P A. y e. B ( x ( .s ` K ) y ) e. B ) ) /\ ( ( q e. P /\ r e. P ) /\ ( z e. B /\ w e. B ) ) ) -> ( ( r ( .s ` K ) w ) e. B <-> ( r ( .s ` L ) w ) e. B ) )
72 simplr1 
 |-  ( ( ( ph /\ ( K e. Grp /\ F e. Ring /\ A. x e. P A. y e. B ( x ( .s ` K ) y ) e. B ) ) /\ ( ( q e. P /\ r e. P ) /\ ( z e. B /\ w e. B ) ) ) -> K e. Grp )
73 1 ad2antrr 
 |-  ( ( ( ph /\ ( K e. Grp /\ F e. Ring /\ A. x e. P A. y e. B ( x ( .s ` K ) y ) e. B ) ) /\ ( ( q e. P /\ r e. P ) /\ ( z e. B /\ w e. B ) ) ) -> B = ( Base ` K ) )
74 68 73 eleqtrd 
 |-  ( ( ( ph /\ ( K e. Grp /\ F e. Ring /\ A. x e. P A. y e. B ( x ( .s ` K ) y ) e. B ) ) /\ ( ( q e. P /\ r e. P ) /\ ( z e. B /\ w e. B ) ) ) -> w e. ( Base ` K ) )
75 simprrl 
 |-  ( ( ( ph /\ ( K e. Grp /\ F e. Ring /\ A. x e. P A. y e. B ( x ( .s ` K ) y ) e. B ) ) /\ ( ( q e. P /\ r e. P ) /\ ( z e. B /\ w e. B ) ) ) -> z e. B )
76 75 73 eleqtrd 
 |-  ( ( ( ph /\ ( K e. Grp /\ F e. Ring /\ A. x e. P A. y e. B ( x ( .s ` K ) y ) e. B ) ) /\ ( ( q e. P /\ r e. P ) /\ ( z e. B /\ w e. B ) ) ) -> z e. ( Base ` K ) )
77 13 14 grpcl 
 |-  ( ( K e. Grp /\ w e. ( Base ` K ) /\ z e. ( Base ` K ) ) -> ( w ( +g ` K ) z ) e. ( Base ` K ) )
78 72 74 76 77 syl3anc 
 |-  ( ( ( ph /\ ( K e. Grp /\ F e. Ring /\ A. x e. P A. y e. B ( x ( .s ` K ) y ) e. B ) ) /\ ( ( q e. P /\ r e. P ) /\ ( z e. B /\ w e. B ) ) ) -> ( w ( +g ` K ) z ) e. ( Base ` K ) )
79 78 73 eleqtrrd 
 |-  ( ( ( ph /\ ( K e. Grp /\ F e. Ring /\ A. x e. P A. y e. B ( x ( .s ` K ) y ) e. B ) ) /\ ( ( q e. P /\ r e. P ) /\ ( z e. B /\ w e. B ) ) ) -> ( w ( +g ` K ) z ) e. B )
80 10 oveqrspc2v 
 |-  ( ( ph /\ ( r e. P /\ ( w ( +g ` K ) z ) e. B ) ) -> ( r ( .s ` K ) ( w ( +g ` K ) z ) ) = ( r ( .s ` L ) ( w ( +g ` K ) z ) ) )
81 66 67 79 80 syl12anc 
 |-  ( ( ( ph /\ ( K e. Grp /\ F e. Ring /\ A. x e. P A. y e. B ( x ( .s ` K ) y ) e. B ) ) /\ ( ( q e. P /\ r e. P ) /\ ( z e. B /\ w e. B ) ) ) -> ( r ( .s ` K ) ( w ( +g ` K ) z ) ) = ( r ( .s ` L ) ( w ( +g ` K ) z ) ) )
82 7 oveqrspc2v 
 |-  ( ( ph /\ ( w e. B /\ z e. B ) ) -> ( w ( +g ` K ) z ) = ( w ( +g ` L ) z ) )
83 66 68 75 82 syl12anc 
 |-  ( ( ( ph /\ ( K e. Grp /\ F e. Ring /\ A. x e. P A. y e. B ( x ( .s ` K ) y ) e. B ) ) /\ ( ( q e. P /\ r e. P ) /\ ( z e. B /\ w e. B ) ) ) -> ( w ( +g ` K ) z ) = ( w ( +g ` L ) z ) )
84 83 oveq2d 
 |-  ( ( ( ph /\ ( K e. Grp /\ F e. Ring /\ A. x e. P A. y e. B ( x ( .s ` K ) y ) e. B ) ) /\ ( ( q e. P /\ r e. P ) /\ ( z e. B /\ w e. B ) ) ) -> ( r ( .s ` L ) ( w ( +g ` K ) z ) ) = ( r ( .s ` L ) ( w ( +g ` L ) z ) ) )
85 81 84 eqtrd 
 |-  ( ( ( ph /\ ( K e. Grp /\ F e. Ring /\ A. x e. P A. y e. B ( x ( .s ` K ) y ) e. B ) ) /\ ( ( q e. P /\ r e. P ) /\ ( z e. B /\ w e. B ) ) ) -> ( r ( .s ` K ) ( w ( +g ` K ) z ) ) = ( r ( .s ` L ) ( w ( +g ` L ) z ) ) )
86 simplr3 
 |-  ( ( ( ph /\ ( K e. Grp /\ F e. Ring /\ A. x e. P A. y e. B ( x ( .s ` K ) y ) e. B ) ) /\ ( ( q e. P /\ r e. P ) /\ ( z e. B /\ w e. B ) ) ) -> A. x e. P A. y e. B ( x ( .s ` K ) y ) e. B )
87 ovrspc2v 
 |-  ( ( ( r e. P /\ w e. B ) /\ A. x e. P A. y e. B ( x ( .s ` K ) y ) e. B ) -> ( r ( .s ` K ) w ) e. B )
88 67 68 86 87 syl21anc 
 |-  ( ( ( ph /\ ( K e. Grp /\ F e. Ring /\ A. x e. P A. y e. B ( x ( .s ` K ) y ) e. B ) ) /\ ( ( q e. P /\ r e. P ) /\ ( z e. B /\ w e. B ) ) ) -> ( r ( .s ` K ) w ) e. B )
89 ovrspc2v 
 |-  ( ( ( r e. P /\ z e. B ) /\ A. x e. P A. y e. B ( x ( .s ` K ) y ) e. B ) -> ( r ( .s ` K ) z ) e. B )
90 67 75 86 89 syl21anc 
 |-  ( ( ( ph /\ ( K e. Grp /\ F e. Ring /\ A. x e. P A. y e. B ( x ( .s ` K ) y ) e. B ) ) /\ ( ( q e. P /\ r e. P ) /\ ( z e. B /\ w e. B ) ) ) -> ( r ( .s ` K ) z ) e. B )
91 7 oveqrspc2v 
 |-  ( ( ph /\ ( ( r ( .s ` K ) w ) e. B /\ ( r ( .s ` K ) z ) e. B ) ) -> ( ( r ( .s ` K ) w ) ( +g ` K ) ( r ( .s ` K ) z ) ) = ( ( r ( .s ` K ) w ) ( +g ` L ) ( r ( .s ` K ) z ) ) )
92 66 88 90 91 syl12anc 
 |-  ( ( ( ph /\ ( K e. Grp /\ F e. Ring /\ A. x e. P A. y e. B ( x ( .s ` K ) y ) e. B ) ) /\ ( ( q e. P /\ r e. P ) /\ ( z e. B /\ w e. B ) ) ) -> ( ( r ( .s ` K ) w ) ( +g ` K ) ( r ( .s ` K ) z ) ) = ( ( r ( .s ` K ) w ) ( +g ` L ) ( r ( .s ` K ) z ) ) )
93 10 oveqrspc2v 
 |-  ( ( ph /\ ( r e. P /\ z e. B ) ) -> ( r ( .s ` K ) z ) = ( r ( .s ` L ) z ) )
94 66 67 75 93 syl12anc 
 |-  ( ( ( ph /\ ( K e. Grp /\ F e. Ring /\ A. x e. P A. y e. B ( x ( .s ` K ) y ) e. B ) ) /\ ( ( q e. P /\ r e. P ) /\ ( z e. B /\ w e. B ) ) ) -> ( r ( .s ` K ) z ) = ( r ( .s ` L ) z ) )
95 70 94 oveq12d 
 |-  ( ( ( ph /\ ( K e. Grp /\ F e. Ring /\ A. x e. P A. y e. B ( x ( .s ` K ) y ) e. B ) ) /\ ( ( q e. P /\ r e. P ) /\ ( z e. B /\ w e. B ) ) ) -> ( ( r ( .s ` K ) w ) ( +g ` L ) ( r ( .s ` K ) z ) ) = ( ( r ( .s ` L ) w ) ( +g ` L ) ( r ( .s ` L ) z ) ) )
96 92 95 eqtrd 
 |-  ( ( ( ph /\ ( K e. Grp /\ F e. Ring /\ A. x e. P A. y e. B ( x ( .s ` K ) y ) e. B ) ) /\ ( ( q e. P /\ r e. P ) /\ ( z e. B /\ w e. B ) ) ) -> ( ( r ( .s ` K ) w ) ( +g ` K ) ( r ( .s ` K ) z ) ) = ( ( r ( .s ` L ) w ) ( +g ` L ) ( r ( .s ` L ) z ) ) )
97 85 96 eqeq12d 
 |-  ( ( ( ph /\ ( K e. Grp /\ F e. Ring /\ A. x e. P A. y e. B ( x ( .s ` K ) y ) e. B ) ) /\ ( ( q e. P /\ r e. P ) /\ ( z e. B /\ w e. B ) ) ) -> ( ( r ( .s ` K ) ( w ( +g ` K ) z ) ) = ( ( r ( .s ` K ) w ) ( +g ` K ) ( r ( .s ` K ) z ) ) <-> ( r ( .s ` L ) ( w ( +g ` L ) z ) ) = ( ( r ( .s ` L ) w ) ( +g ` L ) ( r ( .s ` L ) z ) ) ) )
98 simplr2 
 |-  ( ( ( ph /\ ( K e. Grp /\ F e. Ring /\ A. x e. P A. y e. B ( x ( .s ` K ) y ) e. B ) ) /\ ( ( q e. P /\ r e. P ) /\ ( z e. B /\ w e. B ) ) ) -> F e. Ring )
99 simprll 
 |-  ( ( ( ph /\ ( K e. Grp /\ F e. Ring /\ A. x e. P A. y e. B ( x ( .s ` K ) y ) e. B ) ) /\ ( ( q e. P /\ r e. P ) /\ ( z e. B /\ w e. B ) ) ) -> q e. P )
100 5 ad2antrr 
 |-  ( ( ( ph /\ ( K e. Grp /\ F e. Ring /\ A. x e. P A. y e. B ( x ( .s ` K ) y ) e. B ) ) /\ ( ( q e. P /\ r e. P ) /\ ( z e. B /\ w e. B ) ) ) -> P = ( Base ` F ) )
101 99 100 eleqtrd 
 |-  ( ( ( ph /\ ( K e. Grp /\ F e. Ring /\ A. x e. P A. y e. B ( x ( .s ` K ) y ) e. B ) ) /\ ( ( q e. P /\ r e. P ) /\ ( z e. B /\ w e. B ) ) ) -> q e. ( Base ` F ) )
102 67 100 eleqtrd 
 |-  ( ( ( ph /\ ( K e. Grp /\ F e. Ring /\ A. x e. P A. y e. B ( x ( .s ` K ) y ) e. B ) ) /\ ( ( q e. P /\ r e. P ) /\ ( z e. B /\ w e. B ) ) ) -> r e. ( Base ` F ) )
103 16 17 ringacl 
 |-  ( ( F e. Ring /\ q e. ( Base ` F ) /\ r e. ( Base ` F ) ) -> ( q ( +g ` F ) r ) e. ( Base ` F ) )
104 98 101 102 103 syl3anc 
 |-  ( ( ( ph /\ ( K e. Grp /\ F e. Ring /\ A. x e. P A. y e. B ( x ( .s ` K ) y ) e. B ) ) /\ ( ( q e. P /\ r e. P ) /\ ( z e. B /\ w e. B ) ) ) -> ( q ( +g ` F ) r ) e. ( Base ` F ) )
105 104 100 eleqtrrd 
 |-  ( ( ( ph /\ ( K e. Grp /\ F e. Ring /\ A. x e. P A. y e. B ( x ( .s ` K ) y ) e. B ) ) /\ ( ( q e. P /\ r e. P ) /\ ( z e. B /\ w e. B ) ) ) -> ( q ( +g ` F ) r ) e. P )
106 10 oveqrspc2v 
 |-  ( ( ph /\ ( ( q ( +g ` F ) r ) e. P /\ w e. B ) ) -> ( ( q ( +g ` F ) r ) ( .s ` K ) w ) = ( ( q ( +g ` F ) r ) ( .s ` L ) w ) )
107 66 105 68 106 syl12anc 
 |-  ( ( ( ph /\ ( K e. Grp /\ F e. Ring /\ A. x e. P A. y e. B ( x ( .s ` K ) y ) e. B ) ) /\ ( ( q e. P /\ r e. P ) /\ ( z e. B /\ w e. B ) ) ) -> ( ( q ( +g ` F ) r ) ( .s ` K ) w ) = ( ( q ( +g ` F ) r ) ( .s ` L ) w ) )
108 8 oveqrspc2v 
 |-  ( ( ph /\ ( q e. P /\ r e. P ) ) -> ( q ( +g ` F ) r ) = ( q ( +g ` G ) r ) )
109 108 ad2ant2r 
 |-  ( ( ( ph /\ ( K e. Grp /\ F e. Ring /\ A. x e. P A. y e. B ( x ( .s ` K ) y ) e. B ) ) /\ ( ( q e. P /\ r e. P ) /\ ( z e. B /\ w e. B ) ) ) -> ( q ( +g ` F ) r ) = ( q ( +g ` G ) r ) )
110 109 oveq1d 
 |-  ( ( ( ph /\ ( K e. Grp /\ F e. Ring /\ A. x e. P A. y e. B ( x ( .s ` K ) y ) e. B ) ) /\ ( ( q e. P /\ r e. P ) /\ ( z e. B /\ w e. B ) ) ) -> ( ( q ( +g ` F ) r ) ( .s ` L ) w ) = ( ( q ( +g ` G ) r ) ( .s ` L ) w ) )
111 107 110 eqtrd 
 |-  ( ( ( ph /\ ( K e. Grp /\ F e. Ring /\ A. x e. P A. y e. B ( x ( .s ` K ) y ) e. B ) ) /\ ( ( q e. P /\ r e. P ) /\ ( z e. B /\ w e. B ) ) ) -> ( ( q ( +g ` F ) r ) ( .s ` K ) w ) = ( ( q ( +g ` G ) r ) ( .s ` L ) w ) )
112 ovrspc2v 
 |-  ( ( ( q e. P /\ w e. B ) /\ A. x e. P A. y e. B ( x ( .s ` K ) y ) e. B ) -> ( q ( .s ` K ) w ) e. B )
113 99 68 86 112 syl21anc 
 |-  ( ( ( ph /\ ( K e. Grp /\ F e. Ring /\ A. x e. P A. y e. B ( x ( .s ` K ) y ) e. B ) ) /\ ( ( q e. P /\ r e. P ) /\ ( z e. B /\ w e. B ) ) ) -> ( q ( .s ` K ) w ) e. B )
114 7 oveqrspc2v 
 |-  ( ( ph /\ ( ( q ( .s ` K ) w ) e. B /\ ( r ( .s ` K ) w ) e. B ) ) -> ( ( q ( .s ` K ) w ) ( +g ` K ) ( r ( .s ` K ) w ) ) = ( ( q ( .s ` K ) w ) ( +g ` L ) ( r ( .s ` K ) w ) ) )
115 66 113 88 114 syl12anc 
 |-  ( ( ( ph /\ ( K e. Grp /\ F e. Ring /\ A. x e. P A. y e. B ( x ( .s ` K ) y ) e. B ) ) /\ ( ( q e. P /\ r e. P ) /\ ( z e. B /\ w e. B ) ) ) -> ( ( q ( .s ` K ) w ) ( +g ` K ) ( r ( .s ` K ) w ) ) = ( ( q ( .s ` K ) w ) ( +g ` L ) ( r ( .s ` K ) w ) ) )
116 10 oveqrspc2v 
 |-  ( ( ph /\ ( q e. P /\ w e. B ) ) -> ( q ( .s ` K ) w ) = ( q ( .s ` L ) w ) )
117 66 99 68 116 syl12anc 
 |-  ( ( ( ph /\ ( K e. Grp /\ F e. Ring /\ A. x e. P A. y e. B ( x ( .s ` K ) y ) e. B ) ) /\ ( ( q e. P /\ r e. P ) /\ ( z e. B /\ w e. B ) ) ) -> ( q ( .s ` K ) w ) = ( q ( .s ` L ) w ) )
118 117 70 oveq12d 
 |-  ( ( ( ph /\ ( K e. Grp /\ F e. Ring /\ A. x e. P A. y e. B ( x ( .s ` K ) y ) e. B ) ) /\ ( ( q e. P /\ r e. P ) /\ ( z e. B /\ w e. B ) ) ) -> ( ( q ( .s ` K ) w ) ( +g ` L ) ( r ( .s ` K ) w ) ) = ( ( q ( .s ` L ) w ) ( +g ` L ) ( r ( .s ` L ) w ) ) )
119 115 118 eqtrd 
 |-  ( ( ( ph /\ ( K e. Grp /\ F e. Ring /\ A. x e. P A. y e. B ( x ( .s ` K ) y ) e. B ) ) /\ ( ( q e. P /\ r e. P ) /\ ( z e. B /\ w e. B ) ) ) -> ( ( q ( .s ` K ) w ) ( +g ` K ) ( r ( .s ` K ) w ) ) = ( ( q ( .s ` L ) w ) ( +g ` L ) ( r ( .s ` L ) w ) ) )
120 111 119 eqeq12d 
 |-  ( ( ( ph /\ ( K e. Grp /\ F e. Ring /\ A. x e. P A. y e. B ( x ( .s ` K ) y ) e. B ) ) /\ ( ( q e. P /\ r e. P ) /\ ( z e. B /\ w e. B ) ) ) -> ( ( ( q ( +g ` F ) r ) ( .s ` K ) w ) = ( ( q ( .s ` K ) w ) ( +g ` K ) ( r ( .s ` K ) w ) ) <-> ( ( q ( +g ` G ) r ) ( .s ` L ) w ) = ( ( q ( .s ` L ) w ) ( +g ` L ) ( r ( .s ` L ) w ) ) ) )
121 71 97 120 3anbi123d 
 |-  ( ( ( ph /\ ( K e. Grp /\ F e. Ring /\ A. x e. P A. y e. B ( x ( .s ` K ) y ) e. B ) ) /\ ( ( q e. P /\ r e. P ) /\ ( z e. B /\ w e. B ) ) ) -> ( ( ( r ( .s ` K ) w ) e. B /\ ( r ( .s ` K ) ( w ( +g ` K ) z ) ) = ( ( r ( .s ` K ) w ) ( +g ` K ) ( r ( .s ` K ) z ) ) /\ ( ( q ( +g ` F ) r ) ( .s ` K ) w ) = ( ( q ( .s ` K ) w ) ( +g ` K ) ( r ( .s ` K ) w ) ) ) <-> ( ( r ( .s ` L ) w ) e. B /\ ( r ( .s ` L ) ( w ( +g ` L ) z ) ) = ( ( r ( .s ` L ) w ) ( +g ` L ) ( r ( .s ` L ) z ) ) /\ ( ( q ( +g ` G ) r ) ( .s ` L ) w ) = ( ( q ( .s ` L ) w ) ( +g ` L ) ( r ( .s ` L ) w ) ) ) ) )
122 16 18 ringcl 
 |-  ( ( F e. Ring /\ q e. ( Base ` F ) /\ r e. ( Base ` F ) ) -> ( q ( .r ` F ) r ) e. ( Base ` F ) )
123 98 101 102 122 syl3anc 
 |-  ( ( ( ph /\ ( K e. Grp /\ F e. Ring /\ A. x e. P A. y e. B ( x ( .s ` K ) y ) e. B ) ) /\ ( ( q e. P /\ r e. P ) /\ ( z e. B /\ w e. B ) ) ) -> ( q ( .r ` F ) r ) e. ( Base ` F ) )
124 123 100 eleqtrrd 
 |-  ( ( ( ph /\ ( K e. Grp /\ F e. Ring /\ A. x e. P A. y e. B ( x ( .s ` K ) y ) e. B ) ) /\ ( ( q e. P /\ r e. P ) /\ ( z e. B /\ w e. B ) ) ) -> ( q ( .r ` F ) r ) e. P )
125 10 oveqrspc2v 
 |-  ( ( ph /\ ( ( q ( .r ` F ) r ) e. P /\ w e. B ) ) -> ( ( q ( .r ` F ) r ) ( .s ` K ) w ) = ( ( q ( .r ` F ) r ) ( .s ` L ) w ) )
126 66 124 68 125 syl12anc 
 |-  ( ( ( ph /\ ( K e. Grp /\ F e. Ring /\ A. x e. P A. y e. B ( x ( .s ` K ) y ) e. B ) ) /\ ( ( q e. P /\ r e. P ) /\ ( z e. B /\ w e. B ) ) ) -> ( ( q ( .r ` F ) r ) ( .s ` K ) w ) = ( ( q ( .r ` F ) r ) ( .s ` L ) w ) )
127 9 oveqrspc2v 
 |-  ( ( ph /\ ( q e. P /\ r e. P ) ) -> ( q ( .r ` F ) r ) = ( q ( .r ` G ) r ) )
128 127 ad2ant2r 
 |-  ( ( ( ph /\ ( K e. Grp /\ F e. Ring /\ A. x e. P A. y e. B ( x ( .s ` K ) y ) e. B ) ) /\ ( ( q e. P /\ r e. P ) /\ ( z e. B /\ w e. B ) ) ) -> ( q ( .r ` F ) r ) = ( q ( .r ` G ) r ) )
129 128 oveq1d 
 |-  ( ( ( ph /\ ( K e. Grp /\ F e. Ring /\ A. x e. P A. y e. B ( x ( .s ` K ) y ) e. B ) ) /\ ( ( q e. P /\ r e. P ) /\ ( z e. B /\ w e. B ) ) ) -> ( ( q ( .r ` F ) r ) ( .s ` L ) w ) = ( ( q ( .r ` G ) r ) ( .s ` L ) w ) )
130 126 129 eqtrd 
 |-  ( ( ( ph /\ ( K e. Grp /\ F e. Ring /\ A. x e. P A. y e. B ( x ( .s ` K ) y ) e. B ) ) /\ ( ( q e. P /\ r e. P ) /\ ( z e. B /\ w e. B ) ) ) -> ( ( q ( .r ` F ) r ) ( .s ` K ) w ) = ( ( q ( .r ` G ) r ) ( .s ` L ) w ) )
131 10 oveqrspc2v 
 |-  ( ( ph /\ ( q e. P /\ ( r ( .s ` K ) w ) e. B ) ) -> ( q ( .s ` K ) ( r ( .s ` K ) w ) ) = ( q ( .s ` L ) ( r ( .s ` K ) w ) ) )
132 66 99 88 131 syl12anc 
 |-  ( ( ( ph /\ ( K e. Grp /\ F e. Ring /\ A. x e. P A. y e. B ( x ( .s ` K ) y ) e. B ) ) /\ ( ( q e. P /\ r e. P ) /\ ( z e. B /\ w e. B ) ) ) -> ( q ( .s ` K ) ( r ( .s ` K ) w ) ) = ( q ( .s ` L ) ( r ( .s ` K ) w ) ) )
133 70 oveq2d 
 |-  ( ( ( ph /\ ( K e. Grp /\ F e. Ring /\ A. x e. P A. y e. B ( x ( .s ` K ) y ) e. B ) ) /\ ( ( q e. P /\ r e. P ) /\ ( z e. B /\ w e. B ) ) ) -> ( q ( .s ` L ) ( r ( .s ` K ) w ) ) = ( q ( .s ` L ) ( r ( .s ` L ) w ) ) )
134 132 133 eqtrd 
 |-  ( ( ( ph /\ ( K e. Grp /\ F e. Ring /\ A. x e. P A. y e. B ( x ( .s ` K ) y ) e. B ) ) /\ ( ( q e. P /\ r e. P ) /\ ( z e. B /\ w e. B ) ) ) -> ( q ( .s ` K ) ( r ( .s ` K ) w ) ) = ( q ( .s ` L ) ( r ( .s ` L ) w ) ) )
135 130 134 eqeq12d 
 |-  ( ( ( ph /\ ( K e. Grp /\ F e. Ring /\ A. x e. P A. y e. B ( x ( .s ` K ) y ) e. B ) ) /\ ( ( q e. P /\ r e. P ) /\ ( z e. B /\ w e. B ) ) ) -> ( ( ( q ( .r ` F ) r ) ( .s ` K ) w ) = ( q ( .s ` K ) ( r ( .s ` K ) w ) ) <-> ( ( q ( .r ` G ) r ) ( .s ` L ) w ) = ( q ( .s ` L ) ( r ( .s ` L ) w ) ) ) )
136 16 19 ringidcl 
 |-  ( F e. Ring -> ( 1r ` F ) e. ( Base ` F ) )
137 98 136 syl 
 |-  ( ( ( ph /\ ( K e. Grp /\ F e. Ring /\ A. x e. P A. y e. B ( x ( .s ` K ) y ) e. B ) ) /\ ( ( q e. P /\ r e. P ) /\ ( z e. B /\ w e. B ) ) ) -> ( 1r ` F ) e. ( Base ` F ) )
138 137 100 eleqtrrd 
 |-  ( ( ( ph /\ ( K e. Grp /\ F e. Ring /\ A. x e. P A. y e. B ( x ( .s ` K ) y ) e. B ) ) /\ ( ( q e. P /\ r e. P ) /\ ( z e. B /\ w e. B ) ) ) -> ( 1r ` F ) e. P )
139 10 oveqrspc2v 
 |-  ( ( ph /\ ( ( 1r ` F ) e. P /\ w e. B ) ) -> ( ( 1r ` F ) ( .s ` K ) w ) = ( ( 1r ` F ) ( .s ` L ) w ) )
140 66 138 68 139 syl12anc 
 |-  ( ( ( ph /\ ( K e. Grp /\ F e. Ring /\ A. x e. P A. y e. B ( x ( .s ` K ) y ) e. B ) ) /\ ( ( q e. P /\ r e. P ) /\ ( z e. B /\ w e. B ) ) ) -> ( ( 1r ` F ) ( .s ` K ) w ) = ( ( 1r ` F ) ( .s ` L ) w ) )
141 5 6 9 rngidpropd 
 |-  ( ph -> ( 1r ` F ) = ( 1r ` G ) )
142 141 ad2antrr 
 |-  ( ( ( ph /\ ( K e. Grp /\ F e. Ring /\ A. x e. P A. y e. B ( x ( .s ` K ) y ) e. B ) ) /\ ( ( q e. P /\ r e. P ) /\ ( z e. B /\ w e. B ) ) ) -> ( 1r ` F ) = ( 1r ` G ) )
143 142 oveq1d 
 |-  ( ( ( ph /\ ( K e. Grp /\ F e. Ring /\ A. x e. P A. y e. B ( x ( .s ` K ) y ) e. B ) ) /\ ( ( q e. P /\ r e. P ) /\ ( z e. B /\ w e. B ) ) ) -> ( ( 1r ` F ) ( .s ` L ) w ) = ( ( 1r ` G ) ( .s ` L ) w ) )
144 140 143 eqtrd 
 |-  ( ( ( ph /\ ( K e. Grp /\ F e. Ring /\ A. x e. P A. y e. B ( x ( .s ` K ) y ) e. B ) ) /\ ( ( q e. P /\ r e. P ) /\ ( z e. B /\ w e. B ) ) ) -> ( ( 1r ` F ) ( .s ` K ) w ) = ( ( 1r ` G ) ( .s ` L ) w ) )
145 144 eqeq1d 
 |-  ( ( ( ph /\ ( K e. Grp /\ F e. Ring /\ A. x e. P A. y e. B ( x ( .s ` K ) y ) e. B ) ) /\ ( ( q e. P /\ r e. P ) /\ ( z e. B /\ w e. B ) ) ) -> ( ( ( 1r ` F ) ( .s ` K ) w ) = w <-> ( ( 1r ` G ) ( .s ` L ) w ) = w ) )
146 135 145 anbi12d 
 |-  ( ( ( ph /\ ( K e. Grp /\ F e. Ring /\ A. x e. P A. y e. B ( x ( .s ` K ) y ) e. B ) ) /\ ( ( q e. P /\ r e. P ) /\ ( z e. B /\ w e. B ) ) ) -> ( ( ( ( q ( .r ` F ) r ) ( .s ` K ) w ) = ( q ( .s ` K ) ( r ( .s ` K ) w ) ) /\ ( ( 1r ` F ) ( .s ` K ) w ) = w ) <-> ( ( ( q ( .r ` G ) r ) ( .s ` L ) w ) = ( q ( .s ` L ) ( r ( .s ` L ) w ) ) /\ ( ( 1r ` G ) ( .s ` L ) w ) = w ) ) )
147 121 146 anbi12d 
 |-  ( ( ( ph /\ ( K e. Grp /\ F e. Ring /\ A. x e. P A. y e. B ( x ( .s ` K ) y ) e. B ) ) /\ ( ( q e. P /\ r e. P ) /\ ( z e. B /\ w e. B ) ) ) -> ( ( ( ( r ( .s ` K ) w ) e. B /\ ( r ( .s ` K ) ( w ( +g ` K ) z ) ) = ( ( r ( .s ` K ) w ) ( +g ` K ) ( r ( .s ` K ) z ) ) /\ ( ( q ( +g ` F ) r ) ( .s ` K ) w ) = ( ( q ( .s ` K ) w ) ( +g ` K ) ( r ( .s ` K ) w ) ) ) /\ ( ( ( q ( .r ` F ) r ) ( .s ` K ) w ) = ( q ( .s ` K ) ( r ( .s ` K ) w ) ) /\ ( ( 1r ` F ) ( .s ` K ) w ) = w ) ) <-> ( ( ( r ( .s ` L ) w ) e. B /\ ( r ( .s ` L ) ( w ( +g ` L ) z ) ) = ( ( r ( .s ` L ) w ) ( +g ` L ) ( r ( .s ` L ) z ) ) /\ ( ( q ( +g ` G ) r ) ( .s ` L ) w ) = ( ( q ( .s ` L ) w ) ( +g ` L ) ( r ( .s ` L ) w ) ) ) /\ ( ( ( q ( .r ` G ) r ) ( .s ` L ) w ) = ( q ( .s ` L ) ( r ( .s ` L ) w ) ) /\ ( ( 1r ` G ) ( .s ` L ) w ) = w ) ) ) )
148 147 anassrs 
 |-  ( ( ( ( ph /\ ( K e. Grp /\ F e. Ring /\ A. x e. P A. y e. B ( x ( .s ` K ) y ) e. B ) ) /\ ( q e. P /\ r e. P ) ) /\ ( z e. B /\ w e. B ) ) -> ( ( ( ( r ( .s ` K ) w ) e. B /\ ( r ( .s ` K ) ( w ( +g ` K ) z ) ) = ( ( r ( .s ` K ) w ) ( +g ` K ) ( r ( .s ` K ) z ) ) /\ ( ( q ( +g ` F ) r ) ( .s ` K ) w ) = ( ( q ( .s ` K ) w ) ( +g ` K ) ( r ( .s ` K ) w ) ) ) /\ ( ( ( q ( .r ` F ) r ) ( .s ` K ) w ) = ( q ( .s ` K ) ( r ( .s ` K ) w ) ) /\ ( ( 1r ` F ) ( .s ` K ) w ) = w ) ) <-> ( ( ( r ( .s ` L ) w ) e. B /\ ( r ( .s ` L ) ( w ( +g ` L ) z ) ) = ( ( r ( .s ` L ) w ) ( +g ` L ) ( r ( .s ` L ) z ) ) /\ ( ( q ( +g ` G ) r ) ( .s ` L ) w ) = ( ( q ( .s ` L ) w ) ( +g ` L ) ( r ( .s ` L ) w ) ) ) /\ ( ( ( q ( .r ` G ) r ) ( .s ` L ) w ) = ( q ( .s ` L ) ( r ( .s ` L ) w ) ) /\ ( ( 1r ` G ) ( .s ` L ) w ) = w ) ) ) )
149 148 2ralbidva 
 |-  ( ( ( ph /\ ( K e. Grp /\ F e. Ring /\ A. x e. P A. y e. B ( x ( .s ` K ) y ) e. B ) ) /\ ( q e. P /\ r e. P ) ) -> ( A. z e. B A. w e. B ( ( ( r ( .s ` K ) w ) e. B /\ ( r ( .s ` K ) ( w ( +g ` K ) z ) ) = ( ( r ( .s ` K ) w ) ( +g ` K ) ( r ( .s ` K ) z ) ) /\ ( ( q ( +g ` F ) r ) ( .s ` K ) w ) = ( ( q ( .s ` K ) w ) ( +g ` K ) ( r ( .s ` K ) w ) ) ) /\ ( ( ( q ( .r ` F ) r ) ( .s ` K ) w ) = ( q ( .s ` K ) ( r ( .s ` K ) w ) ) /\ ( ( 1r ` F ) ( .s ` K ) w ) = w ) ) <-> A. z e. B A. w e. B ( ( ( r ( .s ` L ) w ) e. B /\ ( r ( .s ` L ) ( w ( +g ` L ) z ) ) = ( ( r ( .s ` L ) w ) ( +g ` L ) ( r ( .s ` L ) z ) ) /\ ( ( q ( +g ` G ) r ) ( .s ` L ) w ) = ( ( q ( .s ` L ) w ) ( +g ` L ) ( r ( .s ` L ) w ) ) ) /\ ( ( ( q ( .r ` G ) r ) ( .s ` L ) w ) = ( q ( .s ` L ) ( r ( .s ` L ) w ) ) /\ ( ( 1r ` G ) ( .s ` L ) w ) = w ) ) ) )
150 149 2ralbidva 
 |-  ( ( ph /\ ( K e. Grp /\ F e. Ring /\ A. x e. P A. y e. B ( x ( .s ` K ) y ) e. B ) ) -> ( A. q e. P A. r e. P A. z e. B A. w e. B ( ( ( r ( .s ` K ) w ) e. B /\ ( r ( .s ` K ) ( w ( +g ` K ) z ) ) = ( ( r ( .s ` K ) w ) ( +g ` K ) ( r ( .s ` K ) z ) ) /\ ( ( q ( +g ` F ) r ) ( .s ` K ) w ) = ( ( q ( .s ` K ) w ) ( +g ` K ) ( r ( .s ` K ) w ) ) ) /\ ( ( ( q ( .r ` F ) r ) ( .s ` K ) w ) = ( q ( .s ` K ) ( r ( .s ` K ) w ) ) /\ ( ( 1r ` F ) ( .s ` K ) w ) = w ) ) <-> A. q e. P A. r e. P A. z e. B A. w e. B ( ( ( r ( .s ` L ) w ) e. B /\ ( r ( .s ` L ) ( w ( +g ` L ) z ) ) = ( ( r ( .s ` L ) w ) ( +g ` L ) ( r ( .s ` L ) z ) ) /\ ( ( q ( +g ` G ) r ) ( .s ` L ) w ) = ( ( q ( .s ` L ) w ) ( +g ` L ) ( r ( .s ` L ) w ) ) ) /\ ( ( ( q ( .r ` G ) r ) ( .s ` L ) w ) = ( q ( .s ` L ) ( r ( .s ` L ) w ) ) /\ ( ( 1r ` G ) ( .s ` L ) w ) = w ) ) ) )
151 5 adantr 
 |-  ( ( ph /\ ( K e. Grp /\ F e. Ring /\ A. x e. P A. y e. B ( x ( .s ` K ) y ) e. B ) ) -> P = ( Base ` F ) )
152 1 adantr 
 |-  ( ( ph /\ ( K e. Grp /\ F e. Ring /\ A. x e. P A. y e. B ( x ( .s ` K ) y ) e. B ) ) -> B = ( Base ` K ) )
153 152 eleq2d 
 |-  ( ( ph /\ ( K e. Grp /\ F e. Ring /\ A. x e. P A. y e. B ( x ( .s ` K ) y ) e. B ) ) -> ( ( r ( .s ` K ) w ) e. B <-> ( r ( .s ` K ) w ) e. ( Base ` K ) ) )
154 153 3anbi1d 
 |-  ( ( ph /\ ( K e. Grp /\ F e. Ring /\ A. x e. P A. y e. B ( x ( .s ` K ) y ) e. B ) ) -> ( ( ( r ( .s ` K ) w ) e. B /\ ( r ( .s ` K ) ( w ( +g ` K ) z ) ) = ( ( r ( .s ` K ) w ) ( +g ` K ) ( r ( .s ` K ) z ) ) /\ ( ( q ( +g ` F ) r ) ( .s ` K ) w ) = ( ( q ( .s ` K ) w ) ( +g ` K ) ( r ( .s ` K ) w ) ) ) <-> ( ( r ( .s ` K ) w ) e. ( Base ` K ) /\ ( r ( .s ` K ) ( w ( +g ` K ) z ) ) = ( ( r ( .s ` K ) w ) ( +g ` K ) ( r ( .s ` K ) z ) ) /\ ( ( q ( +g ` F ) r ) ( .s ` K ) w ) = ( ( q ( .s ` K ) w ) ( +g ` K ) ( r ( .s ` K ) w ) ) ) ) )
155 154 anbi1d 
 |-  ( ( ph /\ ( K e. Grp /\ F e. Ring /\ A. x e. P A. y e. B ( x ( .s ` K ) y ) e. B ) ) -> ( ( ( ( r ( .s ` K ) w ) e. B /\ ( r ( .s ` K ) ( w ( +g ` K ) z ) ) = ( ( r ( .s ` K ) w ) ( +g ` K ) ( r ( .s ` K ) z ) ) /\ ( ( q ( +g ` F ) r ) ( .s ` K ) w ) = ( ( q ( .s ` K ) w ) ( +g ` K ) ( r ( .s ` K ) w ) ) ) /\ ( ( ( q ( .r ` F ) r ) ( .s ` K ) w ) = ( q ( .s ` K ) ( r ( .s ` K ) w ) ) /\ ( ( 1r ` F ) ( .s ` K ) w ) = w ) ) <-> ( ( ( r ( .s ` K ) w ) e. ( Base ` K ) /\ ( r ( .s ` K ) ( w ( +g ` K ) z ) ) = ( ( r ( .s ` K ) w ) ( +g ` K ) ( r ( .s ` K ) z ) ) /\ ( ( q ( +g ` F ) r ) ( .s ` K ) w ) = ( ( q ( .s ` K ) w ) ( +g ` K ) ( r ( .s ` K ) w ) ) ) /\ ( ( ( q ( .r ` F ) r ) ( .s ` K ) w ) = ( q ( .s ` K ) ( r ( .s ` K ) w ) ) /\ ( ( 1r ` F ) ( .s ` K ) w ) = w ) ) ) )
156 152 155 raleqbidv 
 |-  ( ( ph /\ ( K e. Grp /\ F e. Ring /\ A. x e. P A. y e. B ( x ( .s ` K ) y ) e. B ) ) -> ( A. w e. B ( ( ( r ( .s ` K ) w ) e. B /\ ( r ( .s ` K ) ( w ( +g ` K ) z ) ) = ( ( r ( .s ` K ) w ) ( +g ` K ) ( r ( .s ` K ) z ) ) /\ ( ( q ( +g ` F ) r ) ( .s ` K ) w ) = ( ( q ( .s ` K ) w ) ( +g ` K ) ( r ( .s ` K ) w ) ) ) /\ ( ( ( q ( .r ` F ) r ) ( .s ` K ) w ) = ( q ( .s ` K ) ( r ( .s ` K ) w ) ) /\ ( ( 1r ` F ) ( .s ` K ) w ) = w ) ) <-> A. w e. ( Base ` K ) ( ( ( r ( .s ` K ) w ) e. ( Base ` K ) /\ ( r ( .s ` K ) ( w ( +g ` K ) z ) ) = ( ( r ( .s ` K ) w ) ( +g ` K ) ( r ( .s ` K ) z ) ) /\ ( ( q ( +g ` F ) r ) ( .s ` K ) w ) = ( ( q ( .s ` K ) w ) ( +g ` K ) ( r ( .s ` K ) w ) ) ) /\ ( ( ( q ( .r ` F ) r ) ( .s ` K ) w ) = ( q ( .s ` K ) ( r ( .s ` K ) w ) ) /\ ( ( 1r ` F ) ( .s ` K ) w ) = w ) ) ) )
157 152 156 raleqbidv 
 |-  ( ( ph /\ ( K e. Grp /\ F e. Ring /\ A. x e. P A. y e. B ( x ( .s ` K ) y ) e. B ) ) -> ( A. z e. B A. w e. B ( ( ( r ( .s ` K ) w ) e. B /\ ( r ( .s ` K ) ( w ( +g ` K ) z ) ) = ( ( r ( .s ` K ) w ) ( +g ` K ) ( r ( .s ` K ) z ) ) /\ ( ( q ( +g ` F ) r ) ( .s ` K ) w ) = ( ( q ( .s ` K ) w ) ( +g ` K ) ( r ( .s ` K ) w ) ) ) /\ ( ( ( q ( .r ` F ) r ) ( .s ` K ) w ) = ( q ( .s ` K ) ( r ( .s ` K ) w ) ) /\ ( ( 1r ` F ) ( .s ` K ) w ) = w ) ) <-> A. z e. ( Base ` K ) A. w e. ( Base ` K ) ( ( ( r ( .s ` K ) w ) e. ( Base ` K ) /\ ( r ( .s ` K ) ( w ( +g ` K ) z ) ) = ( ( r ( .s ` K ) w ) ( +g ` K ) ( r ( .s ` K ) z ) ) /\ ( ( q ( +g ` F ) r ) ( .s ` K ) w ) = ( ( q ( .s ` K ) w ) ( +g ` K ) ( r ( .s ` K ) w ) ) ) /\ ( ( ( q ( .r ` F ) r ) ( .s ` K ) w ) = ( q ( .s ` K ) ( r ( .s ` K ) w ) ) /\ ( ( 1r ` F ) ( .s ` K ) w ) = w ) ) ) )
158 151 157 raleqbidv 
 |-  ( ( ph /\ ( K e. Grp /\ F e. Ring /\ A. x e. P A. y e. B ( x ( .s ` K ) y ) e. B ) ) -> ( A. r e. P A. z e. B A. w e. B ( ( ( r ( .s ` K ) w ) e. B /\ ( r ( .s ` K ) ( w ( +g ` K ) z ) ) = ( ( r ( .s ` K ) w ) ( +g ` K ) ( r ( .s ` K ) z ) ) /\ ( ( q ( +g ` F ) r ) ( .s ` K ) w ) = ( ( q ( .s ` K ) w ) ( +g ` K ) ( r ( .s ` K ) w ) ) ) /\ ( ( ( q ( .r ` F ) r ) ( .s ` K ) w ) = ( q ( .s ` K ) ( r ( .s ` K ) w ) ) /\ ( ( 1r ` F ) ( .s ` K ) w ) = w ) ) <-> A. r e. ( Base ` F ) A. z e. ( Base ` K ) A. w e. ( Base ` K ) ( ( ( r ( .s ` K ) w ) e. ( Base ` K ) /\ ( r ( .s ` K ) ( w ( +g ` K ) z ) ) = ( ( r ( .s ` K ) w ) ( +g ` K ) ( r ( .s ` K ) z ) ) /\ ( ( q ( +g ` F ) r ) ( .s ` K ) w ) = ( ( q ( .s ` K ) w ) ( +g ` K ) ( r ( .s ` K ) w ) ) ) /\ ( ( ( q ( .r ` F ) r ) ( .s ` K ) w ) = ( q ( .s ` K ) ( r ( .s ` K ) w ) ) /\ ( ( 1r ` F ) ( .s ` K ) w ) = w ) ) ) )
159 151 158 raleqbidv 
 |-  ( ( ph /\ ( K e. Grp /\ F e. Ring /\ A. x e. P A. y e. B ( x ( .s ` K ) y ) e. B ) ) -> ( A. q e. P A. r e. P A. z e. B A. w e. B ( ( ( r ( .s ` K ) w ) e. B /\ ( r ( .s ` K ) ( w ( +g ` K ) z ) ) = ( ( r ( .s ` K ) w ) ( +g ` K ) ( r ( .s ` K ) z ) ) /\ ( ( q ( +g ` F ) r ) ( .s ` K ) w ) = ( ( q ( .s ` K ) w ) ( +g ` K ) ( r ( .s ` K ) w ) ) ) /\ ( ( ( q ( .r ` F ) r ) ( .s ` K ) w ) = ( q ( .s ` K ) ( r ( .s ` K ) w ) ) /\ ( ( 1r ` F ) ( .s ` K ) w ) = w ) ) <-> A. q e. ( Base ` F ) A. r e. ( Base ` F ) A. z e. ( Base ` K ) A. w e. ( Base ` K ) ( ( ( r ( .s ` K ) w ) e. ( Base ` K ) /\ ( r ( .s ` K ) ( w ( +g ` K ) z ) ) = ( ( r ( .s ` K ) w ) ( +g ` K ) ( r ( .s ` K ) z ) ) /\ ( ( q ( +g ` F ) r ) ( .s ` K ) w ) = ( ( q ( .s ` K ) w ) ( +g ` K ) ( r ( .s ` K ) w ) ) ) /\ ( ( ( q ( .r ` F ) r ) ( .s ` K ) w ) = ( q ( .s ` K ) ( r ( .s ` K ) w ) ) /\ ( ( 1r ` F ) ( .s ` K ) w ) = w ) ) ) )
160 6 adantr 
 |-  ( ( ph /\ ( K e. Grp /\ F e. Ring /\ A. x e. P A. y e. B ( x ( .s ` K ) y ) e. B ) ) -> P = ( Base ` G ) )
161 2 adantr 
 |-  ( ( ph /\ ( K e. Grp /\ F e. Ring /\ A. x e. P A. y e. B ( x ( .s ` K ) y ) e. B ) ) -> B = ( Base ` L ) )
162 161 eleq2d 
 |-  ( ( ph /\ ( K e. Grp /\ F e. Ring /\ A. x e. P A. y e. B ( x ( .s ` K ) y ) e. B ) ) -> ( ( r ( .s ` L ) w ) e. B <-> ( r ( .s ` L ) w ) e. ( Base ` L ) ) )
163 162 3anbi1d 
 |-  ( ( ph /\ ( K e. Grp /\ F e. Ring /\ A. x e. P A. y e. B ( x ( .s ` K ) y ) e. B ) ) -> ( ( ( r ( .s ` L ) w ) e. B /\ ( r ( .s ` L ) ( w ( +g ` L ) z ) ) = ( ( r ( .s ` L ) w ) ( +g ` L ) ( r ( .s ` L ) z ) ) /\ ( ( q ( +g ` G ) r ) ( .s ` L ) w ) = ( ( q ( .s ` L ) w ) ( +g ` L ) ( r ( .s ` L ) w ) ) ) <-> ( ( r ( .s ` L ) w ) e. ( Base ` L ) /\ ( r ( .s ` L ) ( w ( +g ` L ) z ) ) = ( ( r ( .s ` L ) w ) ( +g ` L ) ( r ( .s ` L ) z ) ) /\ ( ( q ( +g ` G ) r ) ( .s ` L ) w ) = ( ( q ( .s ` L ) w ) ( +g ` L ) ( r ( .s ` L ) w ) ) ) ) )
164 163 anbi1d 
 |-  ( ( ph /\ ( K e. Grp /\ F e. Ring /\ A. x e. P A. y e. B ( x ( .s ` K ) y ) e. B ) ) -> ( ( ( ( r ( .s ` L ) w ) e. B /\ ( r ( .s ` L ) ( w ( +g ` L ) z ) ) = ( ( r ( .s ` L ) w ) ( +g ` L ) ( r ( .s ` L ) z ) ) /\ ( ( q ( +g ` G ) r ) ( .s ` L ) w ) = ( ( q ( .s ` L ) w ) ( +g ` L ) ( r ( .s ` L ) w ) ) ) /\ ( ( ( q ( .r ` G ) r ) ( .s ` L ) w ) = ( q ( .s ` L ) ( r ( .s ` L ) w ) ) /\ ( ( 1r ` G ) ( .s ` L ) w ) = w ) ) <-> ( ( ( r ( .s ` L ) w ) e. ( Base ` L ) /\ ( r ( .s ` L ) ( w ( +g ` L ) z ) ) = ( ( r ( .s ` L ) w ) ( +g ` L ) ( r ( .s ` L ) z ) ) /\ ( ( q ( +g ` G ) r ) ( .s ` L ) w ) = ( ( q ( .s ` L ) w ) ( +g ` L ) ( r ( .s ` L ) w ) ) ) /\ ( ( ( q ( .r ` G ) r ) ( .s ` L ) w ) = ( q ( .s ` L ) ( r ( .s ` L ) w ) ) /\ ( ( 1r ` G ) ( .s ` L ) w ) = w ) ) ) )
165 161 164 raleqbidv 
 |-  ( ( ph /\ ( K e. Grp /\ F e. Ring /\ A. x e. P A. y e. B ( x ( .s ` K ) y ) e. B ) ) -> ( A. w e. B ( ( ( r ( .s ` L ) w ) e. B /\ ( r ( .s ` L ) ( w ( +g ` L ) z ) ) = ( ( r ( .s ` L ) w ) ( +g ` L ) ( r ( .s ` L ) z ) ) /\ ( ( q ( +g ` G ) r ) ( .s ` L ) w ) = ( ( q ( .s ` L ) w ) ( +g ` L ) ( r ( .s ` L ) w ) ) ) /\ ( ( ( q ( .r ` G ) r ) ( .s ` L ) w ) = ( q ( .s ` L ) ( r ( .s ` L ) w ) ) /\ ( ( 1r ` G ) ( .s ` L ) w ) = w ) ) <-> A. w e. ( Base ` L ) ( ( ( r ( .s ` L ) w ) e. ( Base ` L ) /\ ( r ( .s ` L ) ( w ( +g ` L ) z ) ) = ( ( r ( .s ` L ) w ) ( +g ` L ) ( r ( .s ` L ) z ) ) /\ ( ( q ( +g ` G ) r ) ( .s ` L ) w ) = ( ( q ( .s ` L ) w ) ( +g ` L ) ( r ( .s ` L ) w ) ) ) /\ ( ( ( q ( .r ` G ) r ) ( .s ` L ) w ) = ( q ( .s ` L ) ( r ( .s ` L ) w ) ) /\ ( ( 1r ` G ) ( .s ` L ) w ) = w ) ) ) )
166 161 165 raleqbidv 
 |-  ( ( ph /\ ( K e. Grp /\ F e. Ring /\ A. x e. P A. y e. B ( x ( .s ` K ) y ) e. B ) ) -> ( A. z e. B A. w e. B ( ( ( r ( .s ` L ) w ) e. B /\ ( r ( .s ` L ) ( w ( +g ` L ) z ) ) = ( ( r ( .s ` L ) w ) ( +g ` L ) ( r ( .s ` L ) z ) ) /\ ( ( q ( +g ` G ) r ) ( .s ` L ) w ) = ( ( q ( .s ` L ) w ) ( +g ` L ) ( r ( .s ` L ) w ) ) ) /\ ( ( ( q ( .r ` G ) r ) ( .s ` L ) w ) = ( q ( .s ` L ) ( r ( .s ` L ) w ) ) /\ ( ( 1r ` G ) ( .s ` L ) w ) = w ) ) <-> A. z e. ( Base ` L ) A. w e. ( Base ` L ) ( ( ( r ( .s ` L ) w ) e. ( Base ` L ) /\ ( r ( .s ` L ) ( w ( +g ` L ) z ) ) = ( ( r ( .s ` L ) w ) ( +g ` L ) ( r ( .s ` L ) z ) ) /\ ( ( q ( +g ` G ) r ) ( .s ` L ) w ) = ( ( q ( .s ` L ) w ) ( +g ` L ) ( r ( .s ` L ) w ) ) ) /\ ( ( ( q ( .r ` G ) r ) ( .s ` L ) w ) = ( q ( .s ` L ) ( r ( .s ` L ) w ) ) /\ ( ( 1r ` G ) ( .s ` L ) w ) = w ) ) ) )
167 160 166 raleqbidv 
 |-  ( ( ph /\ ( K e. Grp /\ F e. Ring /\ A. x e. P A. y e. B ( x ( .s ` K ) y ) e. B ) ) -> ( A. r e. P A. z e. B A. w e. B ( ( ( r ( .s ` L ) w ) e. B /\ ( r ( .s ` L ) ( w ( +g ` L ) z ) ) = ( ( r ( .s ` L ) w ) ( +g ` L ) ( r ( .s ` L ) z ) ) /\ ( ( q ( +g ` G ) r ) ( .s ` L ) w ) = ( ( q ( .s ` L ) w ) ( +g ` L ) ( r ( .s ` L ) w ) ) ) /\ ( ( ( q ( .r ` G ) r ) ( .s ` L ) w ) = ( q ( .s ` L ) ( r ( .s ` L ) w ) ) /\ ( ( 1r ` G ) ( .s ` L ) w ) = w ) ) <-> A. r e. ( Base ` G ) A. z e. ( Base ` L ) A. w e. ( Base ` L ) ( ( ( r ( .s ` L ) w ) e. ( Base ` L ) /\ ( r ( .s ` L ) ( w ( +g ` L ) z ) ) = ( ( r ( .s ` L ) w ) ( +g ` L ) ( r ( .s ` L ) z ) ) /\ ( ( q ( +g ` G ) r ) ( .s ` L ) w ) = ( ( q ( .s ` L ) w ) ( +g ` L ) ( r ( .s ` L ) w ) ) ) /\ ( ( ( q ( .r ` G ) r ) ( .s ` L ) w ) = ( q ( .s ` L ) ( r ( .s ` L ) w ) ) /\ ( ( 1r ` G ) ( .s ` L ) w ) = w ) ) ) )
168 160 167 raleqbidv 
 |-  ( ( ph /\ ( K e. Grp /\ F e. Ring /\ A. x e. P A. y e. B ( x ( .s ` K ) y ) e. B ) ) -> ( A. q e. P A. r e. P A. z e. B A. w e. B ( ( ( r ( .s ` L ) w ) e. B /\ ( r ( .s ` L ) ( w ( +g ` L ) z ) ) = ( ( r ( .s ` L ) w ) ( +g ` L ) ( r ( .s ` L ) z ) ) /\ ( ( q ( +g ` G ) r ) ( .s ` L ) w ) = ( ( q ( .s ` L ) w ) ( +g ` L ) ( r ( .s ` L ) w ) ) ) /\ ( ( ( q ( .r ` G ) r ) ( .s ` L ) w ) = ( q ( .s ` L ) ( r ( .s ` L ) w ) ) /\ ( ( 1r ` G ) ( .s ` L ) w ) = w ) ) <-> A. q e. ( Base ` G ) A. r e. ( Base ` G ) A. z e. ( Base ` L ) A. w e. ( Base ` L ) ( ( ( r ( .s ` L ) w ) e. ( Base ` L ) /\ ( r ( .s ` L ) ( w ( +g ` L ) z ) ) = ( ( r ( .s ` L ) w ) ( +g ` L ) ( r ( .s ` L ) z ) ) /\ ( ( q ( +g ` G ) r ) ( .s ` L ) w ) = ( ( q ( .s ` L ) w ) ( +g ` L ) ( r ( .s ` L ) w ) ) ) /\ ( ( ( q ( .r ` G ) r ) ( .s ` L ) w ) = ( q ( .s ` L ) ( r ( .s ` L ) w ) ) /\ ( ( 1r ` G ) ( .s ` L ) w ) = w ) ) ) )
169 150 159 168 3bitr3d 
 |-  ( ( ph /\ ( K e. Grp /\ F e. Ring /\ A. x e. P A. y e. B ( x ( .s ` K ) y ) e. B ) ) -> ( A. q e. ( Base ` F ) A. r e. ( Base ` F ) A. z e. ( Base ` K ) A. w e. ( Base ` K ) ( ( ( r ( .s ` K ) w ) e. ( Base ` K ) /\ ( r ( .s ` K ) ( w ( +g ` K ) z ) ) = ( ( r ( .s ` K ) w ) ( +g ` K ) ( r ( .s ` K ) z ) ) /\ ( ( q ( +g ` F ) r ) ( .s ` K ) w ) = ( ( q ( .s ` K ) w ) ( +g ` K ) ( r ( .s ` K ) w ) ) ) /\ ( ( ( q ( .r ` F ) r ) ( .s ` K ) w ) = ( q ( .s ` K ) ( r ( .s ` K ) w ) ) /\ ( ( 1r ` F ) ( .s ` K ) w ) = w ) ) <-> A. q e. ( Base ` G ) A. r e. ( Base ` G ) A. z e. ( Base ` L ) A. w e. ( Base ` L ) ( ( ( r ( .s ` L ) w ) e. ( Base ` L ) /\ ( r ( .s ` L ) ( w ( +g ` L ) z ) ) = ( ( r ( .s ` L ) w ) ( +g ` L ) ( r ( .s ` L ) z ) ) /\ ( ( q ( +g ` G ) r ) ( .s ` L ) w ) = ( ( q ( .s ` L ) w ) ( +g ` L ) ( r ( .s ` L ) w ) ) ) /\ ( ( ( q ( .r ` G ) r ) ( .s ` L ) w ) = ( q ( .s ` L ) ( r ( .s ` L ) w ) ) /\ ( ( 1r ` G ) ( .s ` L ) w ) = w ) ) ) )
170 64 65 169 3anbi123d 
 |-  ( ( ph /\ ( K e. Grp /\ F e. Ring /\ A. x e. P A. y e. B ( x ( .s ` K ) y ) e. B ) ) -> ( ( K e. Grp /\ F e. Ring /\ A. q e. ( Base ` F ) A. r e. ( Base ` F ) A. z e. ( Base ` K ) A. w e. ( Base ` K ) ( ( ( r ( .s ` K ) w ) e. ( Base ` K ) /\ ( r ( .s ` K ) ( w ( +g ` K ) z ) ) = ( ( r ( .s ` K ) w ) ( +g ` K ) ( r ( .s ` K ) z ) ) /\ ( ( q ( +g ` F ) r ) ( .s ` K ) w ) = ( ( q ( .s ` K ) w ) ( +g ` K ) ( r ( .s ` K ) w ) ) ) /\ ( ( ( q ( .r ` F ) r ) ( .s ` K ) w ) = ( q ( .s ` K ) ( r ( .s ` K ) w ) ) /\ ( ( 1r ` F ) ( .s ` K ) w ) = w ) ) ) <-> ( L e. Grp /\ G e. Ring /\ A. q e. ( Base ` G ) A. r e. ( Base ` G ) A. z e. ( Base ` L ) A. w e. ( Base ` L ) ( ( ( r ( .s ` L ) w ) e. ( Base ` L ) /\ ( r ( .s ` L ) ( w ( +g ` L ) z ) ) = ( ( r ( .s ` L ) w ) ( +g ` L ) ( r ( .s ` L ) z ) ) /\ ( ( q ( +g ` G ) r ) ( .s ` L ) w ) = ( ( q ( .s ` L ) w ) ( +g ` L ) ( r ( .s ` L ) w ) ) ) /\ ( ( ( q ( .r ` G ) r ) ( .s ` L ) w ) = ( q ( .s ` L ) ( r ( .s ` L ) w ) ) /\ ( ( 1r ` G ) ( .s ` L ) w ) = w ) ) ) ) )
171 170 20 46 3bitr4g 
 |-  ( ( ph /\ ( K e. Grp /\ F e. Ring /\ A. x e. P A. y e. B ( x ( .s ` K ) y ) e. B ) ) -> ( K e. LMod <-> L e. LMod ) )
172 171 ex 
 |-  ( ph -> ( ( K e. Grp /\ F e. Ring /\ A. x e. P A. y e. B ( x ( .s ` K ) y ) e. B ) -> ( K e. LMod <-> L e. LMod ) ) )
173 35 63 172 pm5.21ndd 
 |-  ( ph -> ( K e. LMod <-> L e. LMod ) )