Metamath Proof Explorer

Theorem assapropd

Description: If two structures have the same components (properties), one is an associative algebra iff the other one is. (Contributed by Mario Carneiro, 8-Feb-2015)

Ref Expression
Hypotheses assapropd.1 
|- ( ph -> B = ( Base ` K ) )
assapropd.2 
|- ( ph -> B = ( Base ` L ) )
assapropd.3 
|- ( ( ph /\ ( x e. B /\ y e. B ) ) -> ( x ( +g ` K ) y ) = ( x ( +g ` L ) y ) )
assapropd.4 
|- ( ( ph /\ ( x e. B /\ y e. B ) ) -> ( x ( .r ` K ) y ) = ( x ( .r ` L ) y ) )
assapropd.5 
|- ( ph -> F = ( Scalar ` K ) )
assapropd.6 
|- ( ph -> F = ( Scalar ` L ) )
assapropd.7 
|- P = ( Base ` F )
assapropd.8 
|- ( ( ph /\ ( x e. P /\ y e. B ) ) -> ( x ( .s ` K ) y ) = ( x ( .s ` L ) y ) )
Assertion assapropd 
|- ( ph -> ( K e. AssAlg <-> L e. AssAlg ) )

Proof

Step Hyp Ref Expression
1 assapropd.1 
 |-  ( ph -> B = ( Base ` K ) )
2 assapropd.2 
 |-  ( ph -> B = ( Base ` L ) )
3 assapropd.3 
 |-  ( ( ph /\ ( x e. B /\ y e. B ) ) -> ( x ( +g ` K ) y ) = ( x ( +g ` L ) y ) )
4 assapropd.4 
 |-  ( ( ph /\ ( x e. B /\ y e. B ) ) -> ( x ( .r ` K ) y ) = ( x ( .r ` L ) y ) )
5 assapropd.5 
 |-  ( ph -> F = ( Scalar ` K ) )
6 assapropd.6 
 |-  ( ph -> F = ( Scalar ` L ) )
7 assapropd.7 
 |-  P = ( Base ` F )
8 assapropd.8 
 |-  ( ( ph /\ ( x e. P /\ y e. B ) ) -> ( x ( .s ` K ) y ) = ( x ( .s ` L ) y ) )
9 assalmod 
 |-  ( K e. AssAlg -> K e. LMod )
10 assaring 
 |-  ( K e. AssAlg -> K e. Ring )
11 9 10 jca 
 |-  ( K e. AssAlg -> ( K e. LMod /\ K e. Ring ) )
12 11 a1i 
 |-  ( ph -> ( K e. AssAlg -> ( K e. LMod /\ K e. Ring ) ) )
13 assalmod 
 |-  ( L e. AssAlg -> L e. LMod )
14 1 2 3 5 6 7 8 lmodpropd 
 |-  ( ph -> ( K e. LMod <-> L e. LMod ) )
15 13 14 syl5ibr 
 |-  ( ph -> ( L e. AssAlg -> K e. LMod ) )
16 assaring 
 |-  ( L e. AssAlg -> L e. Ring )
17 1 2 3 4 ringpropd 
 |-  ( ph -> ( K e. Ring <-> L e. Ring ) )
18 16 17 syl5ibr 
 |-  ( ph -> ( L e. AssAlg -> K e. Ring ) )
19 15 18 jcad 
 |-  ( ph -> ( L e. AssAlg -> ( K e. LMod /\ K e. Ring ) ) )
20 5 6 eqtr3d 
 |-  ( ph -> ( Scalar ` K ) = ( Scalar ` L ) )
21 20 eleq1d 
 |-  ( ph -> ( ( Scalar ` K ) e. CRing <-> ( Scalar ` L ) e. CRing ) )
22 14 17 21 3anbi123d 
 |-  ( ph -> ( ( K e. LMod /\ K e. Ring /\ ( Scalar ` K ) e. CRing ) <-> ( L e. LMod /\ L e. Ring /\ ( Scalar ` L ) e. CRing ) ) )
23 22 adantr 
 |-  ( ( ph /\ ( K e. LMod /\ K e. Ring ) ) -> ( ( K e. LMod /\ K e. Ring /\ ( Scalar ` K ) e. CRing ) <-> ( L e. LMod /\ L e. Ring /\ ( Scalar ` L ) e. CRing ) ) )
24 simpll 
 |-  ( ( ( ph /\ ( K e. LMod /\ K e. Ring ) ) /\ ( r e. P /\ ( z e. B /\ w e. B ) ) ) -> ph )
25 simplrl 
 |-  ( ( ( ph /\ ( K e. LMod /\ K e. Ring ) ) /\ ( r e. P /\ ( z e. B /\ w e. B ) ) ) -> K e. LMod )
26 simprl 
 |-  ( ( ( ph /\ ( K e. LMod /\ K e. Ring ) ) /\ ( r e. P /\ ( z e. B /\ w e. B ) ) ) -> r e. P )
27 5 fveq2d 
 |-  ( ph -> ( Base ` F ) = ( Base ` ( Scalar ` K ) ) )
28 7 27 syl5eq 
 |-  ( ph -> P = ( Base ` ( Scalar ` K ) ) )
29 24 28 syl 
 |-  ( ( ( ph /\ ( K e. LMod /\ K e. Ring ) ) /\ ( r e. P /\ ( z e. B /\ w e. B ) ) ) -> P = ( Base ` ( Scalar ` K ) ) )
30 26 29 eleqtrd 
 |-  ( ( ( ph /\ ( K e. LMod /\ K e. Ring ) ) /\ ( r e. P /\ ( z e. B /\ w e. B ) ) ) -> r e. ( Base ` ( Scalar ` K ) ) )
31 simprrl 
 |-  ( ( ( ph /\ ( K e. LMod /\ K e. Ring ) ) /\ ( r e. P /\ ( z e. B /\ w e. B ) ) ) -> z e. B )
32 24 1 syl 
 |-  ( ( ( ph /\ ( K e. LMod /\ K e. Ring ) ) /\ ( r e. P /\ ( z e. B /\ w e. B ) ) ) -> B = ( Base ` K ) )
33 31 32 eleqtrd 
 |-  ( ( ( ph /\ ( K e. LMod /\ K e. Ring ) ) /\ ( r e. P /\ ( z e. B /\ w e. B ) ) ) -> z e. ( Base ` K ) )
34 eqid 
 |-  ( Base ` K ) = ( Base ` K )
35 eqid 
 |-  ( Scalar ` K ) = ( Scalar ` K )
36 eqid 
 |-  ( .s ` K ) = ( .s ` K )
37 eqid 
 |-  ( Base ` ( Scalar ` K ) ) = ( Base ` ( Scalar ` K ) )
38 34 35 36 37 lmodvscl 
 |-  ( ( K e. LMod /\ r e. ( Base ` ( Scalar ` K ) ) /\ z e. ( Base ` K ) ) -> ( r ( .s ` K ) z ) e. ( Base ` K ) )
39 25 30 33 38 syl3anc 
 |-  ( ( ( ph /\ ( K e. LMod /\ K e. Ring ) ) /\ ( r e. P /\ ( z e. B /\ w e. B ) ) ) -> ( r ( .s ` K ) z ) e. ( Base ` K ) )
40 39 32 eleqtrrd 
 |-  ( ( ( ph /\ ( K e. LMod /\ K e. Ring ) ) /\ ( r e. P /\ ( z e. B /\ w e. B ) ) ) -> ( r ( .s ` K ) z ) e. B )
41 simprrr 
 |-  ( ( ( ph /\ ( K e. LMod /\ K e. Ring ) ) /\ ( r e. P /\ ( z e. B /\ w e. B ) ) ) -> w e. B )
42 4 oveqrspc2v 
 |-  ( ( ph /\ ( ( r ( .s ` K ) z ) e. B /\ w e. B ) ) -> ( ( r ( .s ` K ) z ) ( .r ` K ) w ) = ( ( r ( .s ` K ) z ) ( .r ` L ) w ) )
43 24 40 41 42 syl12anc 
 |-  ( ( ( ph /\ ( K e. LMod /\ K e. Ring ) ) /\ ( r e. P /\ ( z e. B /\ w e. B ) ) ) -> ( ( r ( .s ` K ) z ) ( .r ` K ) w ) = ( ( r ( .s ` K ) z ) ( .r ` L ) w ) )
44 8 oveqrspc2v 
 |-  ( ( ph /\ ( r e. P /\ z e. B ) ) -> ( r ( .s ` K ) z ) = ( r ( .s ` L ) z ) )
45 24 26 31 44 syl12anc 
 |-  ( ( ( ph /\ ( K e. LMod /\ K e. Ring ) ) /\ ( r e. P /\ ( z e. B /\ w e. B ) ) ) -> ( r ( .s ` K ) z ) = ( r ( .s ` L ) z ) )
46 45 oveq1d 
 |-  ( ( ( ph /\ ( K e. LMod /\ K e. Ring ) ) /\ ( r e. P /\ ( z e. B /\ w e. B ) ) ) -> ( ( r ( .s ` K ) z ) ( .r ` L ) w ) = ( ( r ( .s ` L ) z ) ( .r ` L ) w ) )
47 43 46 eqtrd 
 |-  ( ( ( ph /\ ( K e. LMod /\ K e. Ring ) ) /\ ( r e. P /\ ( z e. B /\ w e. B ) ) ) -> ( ( r ( .s ` K ) z ) ( .r ` K ) w ) = ( ( r ( .s ` L ) z ) ( .r ` L ) w ) )
48 simplrr 
 |-  ( ( ( ph /\ ( K e. LMod /\ K e. Ring ) ) /\ ( r e. P /\ ( z e. B /\ w e. B ) ) ) -> K e. Ring )
49 41 32 eleqtrd 
 |-  ( ( ( ph /\ ( K e. LMod /\ K e. Ring ) ) /\ ( r e. P /\ ( z e. B /\ w e. B ) ) ) -> w e. ( Base ` K ) )
50 eqid 
 |-  ( .r ` K ) = ( .r ` K )
51 34 50 ringcl 
 |-  ( ( K e. Ring /\ z e. ( Base ` K ) /\ w e. ( Base ` K ) ) -> ( z ( .r ` K ) w ) e. ( Base ` K ) )
52 48 33 49 51 syl3anc 
 |-  ( ( ( ph /\ ( K e. LMod /\ K e. Ring ) ) /\ ( r e. P /\ ( z e. B /\ w e. B ) ) ) -> ( z ( .r ` K ) w ) e. ( Base ` K ) )
53 52 32 eleqtrrd 
 |-  ( ( ( ph /\ ( K e. LMod /\ K e. Ring ) ) /\ ( r e. P /\ ( z e. B /\ w e. B ) ) ) -> ( z ( .r ` K ) w ) e. B )
54 8 oveqrspc2v 
 |-  ( ( ph /\ ( r e. P /\ ( z ( .r ` K ) w ) e. B ) ) -> ( r ( .s ` K ) ( z ( .r ` K ) w ) ) = ( r ( .s ` L ) ( z ( .r ` K ) w ) ) )
55 24 26 53 54 syl12anc 
 |-  ( ( ( ph /\ ( K e. LMod /\ K e. Ring ) ) /\ ( r e. P /\ ( z e. B /\ w e. B ) ) ) -> ( r ( .s ` K ) ( z ( .r ` K ) w ) ) = ( r ( .s ` L ) ( z ( .r ` K ) w ) ) )
56 4 oveqrspc2v 
 |-  ( ( ph /\ ( z e. B /\ w e. B ) ) -> ( z ( .r ` K ) w ) = ( z ( .r ` L ) w ) )
57 24 31 41 56 syl12anc 
 |-  ( ( ( ph /\ ( K e. LMod /\ K e. Ring ) ) /\ ( r e. P /\ ( z e. B /\ w e. B ) ) ) -> ( z ( .r ` K ) w ) = ( z ( .r ` L ) w ) )
58 57 oveq2d 
 |-  ( ( ( ph /\ ( K e. LMod /\ K e. Ring ) ) /\ ( r e. P /\ ( z e. B /\ w e. B ) ) ) -> ( r ( .s ` L ) ( z ( .r ` K ) w ) ) = ( r ( .s ` L ) ( z ( .r ` L ) w ) ) )
59 55 58 eqtrd 
 |-  ( ( ( ph /\ ( K e. LMod /\ K e. Ring ) ) /\ ( r e. P /\ ( z e. B /\ w e. B ) ) ) -> ( r ( .s ` K ) ( z ( .r ` K ) w ) ) = ( r ( .s ` L ) ( z ( .r ` L ) w ) ) )
60 47 59 eqeq12d 
 |-  ( ( ( ph /\ ( K e. LMod /\ K e. Ring ) ) /\ ( r e. P /\ ( z e. B /\ w e. B ) ) ) -> ( ( ( r ( .s ` K ) z ) ( .r ` K ) w ) = ( r ( .s ` K ) ( z ( .r ` K ) w ) ) <-> ( ( r ( .s ` L ) z ) ( .r ` L ) w ) = ( r ( .s ` L ) ( z ( .r ` L ) w ) ) ) )
61 34 35 36 37 lmodvscl 
 |-  ( ( K e. LMod /\ r e. ( Base ` ( Scalar ` K ) ) /\ w e. ( Base ` K ) ) -> ( r ( .s ` K ) w ) e. ( Base ` K ) )
62 25 30 49 61 syl3anc 
 |-  ( ( ( ph /\ ( K e. LMod /\ K e. Ring ) ) /\ ( r e. P /\ ( z e. B /\ w e. B ) ) ) -> ( r ( .s ` K ) w ) e. ( Base ` K ) )
63 62 32 eleqtrrd 
 |-  ( ( ( ph /\ ( K e. LMod /\ K e. Ring ) ) /\ ( r e. P /\ ( z e. B /\ w e. B ) ) ) -> ( r ( .s ` K ) w ) e. B )
64 4 oveqrspc2v 
 |-  ( ( ph /\ ( z e. B /\ ( r ( .s ` K ) w ) e. B ) ) -> ( z ( .r ` K ) ( r ( .s ` K ) w ) ) = ( z ( .r ` L ) ( r ( .s ` K ) w ) ) )
65 24 31 63 64 syl12anc 
 |-  ( ( ( ph /\ ( K e. LMod /\ K e. Ring ) ) /\ ( r e. P /\ ( z e. B /\ w e. B ) ) ) -> ( z ( .r ` K ) ( r ( .s ` K ) w ) ) = ( z ( .r ` L ) ( r ( .s ` K ) w ) ) )
66 8 oveqrspc2v 
 |-  ( ( ph /\ ( r e. P /\ w e. B ) ) -> ( r ( .s ` K ) w ) = ( r ( .s ` L ) w ) )
67 24 26 41 66 syl12anc 
 |-  ( ( ( ph /\ ( K e. LMod /\ K e. Ring ) ) /\ ( r e. P /\ ( z e. B /\ w e. B ) ) ) -> ( r ( .s ` K ) w ) = ( r ( .s ` L ) w ) )
68 67 oveq2d 
 |-  ( ( ( ph /\ ( K e. LMod /\ K e. Ring ) ) /\ ( r e. P /\ ( z e. B /\ w e. B ) ) ) -> ( z ( .r ` L ) ( r ( .s ` K ) w ) ) = ( z ( .r ` L ) ( r ( .s ` L ) w ) ) )
69 65 68 eqtrd 
 |-  ( ( ( ph /\ ( K e. LMod /\ K e. Ring ) ) /\ ( r e. P /\ ( z e. B /\ w e. B ) ) ) -> ( z ( .r ` K ) ( r ( .s ` K ) w ) ) = ( z ( .r ` L ) ( r ( .s ` L ) w ) ) )
70 69 59 eqeq12d 
 |-  ( ( ( ph /\ ( K e. LMod /\ K e. Ring ) ) /\ ( r e. P /\ ( z e. B /\ w e. B ) ) ) -> ( ( z ( .r ` K ) ( r ( .s ` K ) w ) ) = ( r ( .s ` K ) ( z ( .r ` K ) w ) ) <-> ( z ( .r ` L ) ( r ( .s ` L ) w ) ) = ( r ( .s ` L ) ( z ( .r ` L ) w ) ) ) )
71 60 70 anbi12d 
 |-  ( ( ( ph /\ ( K e. LMod /\ K e. Ring ) ) /\ ( r e. P /\ ( z e. B /\ w e. B ) ) ) -> ( ( ( ( r ( .s ` K ) z ) ( .r ` K ) w ) = ( r ( .s ` K ) ( z ( .r ` K ) w ) ) /\ ( z ( .r ` K ) ( r ( .s ` K ) w ) ) = ( r ( .s ` K ) ( z ( .r ` K ) w ) ) ) <-> ( ( ( r ( .s ` L ) z ) ( .r ` L ) w ) = ( r ( .s ` L ) ( z ( .r ` L ) w ) ) /\ ( z ( .r ` L ) ( r ( .s ` L ) w ) ) = ( r ( .s ` L ) ( z ( .r ` L ) w ) ) ) ) )
72 71 anassrs 
 |-  ( ( ( ( ph /\ ( K e. LMod /\ K e. Ring ) ) /\ r e. P ) /\ ( z e. B /\ w e. B ) ) -> ( ( ( ( r ( .s ` K ) z ) ( .r ` K ) w ) = ( r ( .s ` K ) ( z ( .r ` K ) w ) ) /\ ( z ( .r ` K ) ( r ( .s ` K ) w ) ) = ( r ( .s ` K ) ( z ( .r ` K ) w ) ) ) <-> ( ( ( r ( .s ` L ) z ) ( .r ` L ) w ) = ( r ( .s ` L ) ( z ( .r ` L ) w ) ) /\ ( z ( .r ` L ) ( r ( .s ` L ) w ) ) = ( r ( .s ` L ) ( z ( .r ` L ) w ) ) ) ) )
73 72 2ralbidva 
 |-  ( ( ( ph /\ ( K e. LMod /\ K e. Ring ) ) /\ r e. P ) -> ( A. z e. B A. w e. B ( ( ( r ( .s ` K ) z ) ( .r ` K ) w ) = ( r ( .s ` K ) ( z ( .r ` K ) w ) ) /\ ( z ( .r ` K ) ( r ( .s ` K ) w ) ) = ( r ( .s ` K ) ( z ( .r ` K ) w ) ) ) <-> A. z e. B A. w e. B ( ( ( r ( .s ` L ) z ) ( .r ` L ) w ) = ( r ( .s ` L ) ( z ( .r ` L ) w ) ) /\ ( z ( .r ` L ) ( r ( .s ` L ) w ) ) = ( r ( .s ` L ) ( z ( .r ` L ) w ) ) ) ) )
74 73 ralbidva 
 |-  ( ( ph /\ ( K e. LMod /\ K e. Ring ) ) -> ( A. r e. P A. z e. B A. w e. B ( ( ( r ( .s ` K ) z ) ( .r ` K ) w ) = ( r ( .s ` K ) ( z ( .r ` K ) w ) ) /\ ( z ( .r ` K ) ( r ( .s ` K ) w ) ) = ( r ( .s ` K ) ( z ( .r ` K ) w ) ) ) <-> A. r e. P A. z e. B A. w e. B ( ( ( r ( .s ` L ) z ) ( .r ` L ) w ) = ( r ( .s ` L ) ( z ( .r ` L ) w ) ) /\ ( z ( .r ` L ) ( r ( .s ` L ) w ) ) = ( r ( .s ` L ) ( z ( .r ` L ) w ) ) ) ) )
75 28 adantr 
 |-  ( ( ph /\ ( K e. LMod /\ K e. Ring ) ) -> P = ( Base ` ( Scalar ` K ) ) )
76 1 adantr 
 |-  ( ( ph /\ ( K e. LMod /\ K e. Ring ) ) -> B = ( Base ` K ) )
77 76 raleqdv 
 |-  ( ( ph /\ ( K e. LMod /\ K e. Ring ) ) -> ( A. w e. B ( ( ( r ( .s ` K ) z ) ( .r ` K ) w ) = ( r ( .s ` K ) ( z ( .r ` K ) w ) ) /\ ( z ( .r ` K ) ( r ( .s ` K ) w ) ) = ( r ( .s ` K ) ( z ( .r ` K ) w ) ) ) <-> A. w e. ( Base ` K ) ( ( ( r ( .s ` K ) z ) ( .r ` K ) w ) = ( r ( .s ` K ) ( z ( .r ` K ) w ) ) /\ ( z ( .r ` K ) ( r ( .s ` K ) w ) ) = ( r ( .s ` K ) ( z ( .r ` K ) w ) ) ) ) )
78 76 77 raleqbidv 
 |-  ( ( ph /\ ( K e. LMod /\ K e. Ring ) ) -> ( A. z e. B A. w e. B ( ( ( r ( .s ` K ) z ) ( .r ` K ) w ) = ( r ( .s ` K ) ( z ( .r ` K ) w ) ) /\ ( z ( .r ` K ) ( r ( .s ` K ) w ) ) = ( r ( .s ` K ) ( z ( .r ` K ) w ) ) ) <-> A. z e. ( Base ` K ) A. w e. ( Base ` K ) ( ( ( r ( .s ` K ) z ) ( .r ` K ) w ) = ( r ( .s ` K ) ( z ( .r ` K ) w ) ) /\ ( z ( .r ` K ) ( r ( .s ` K ) w ) ) = ( r ( .s ` K ) ( z ( .r ` K ) w ) ) ) ) )
79 75 78 raleqbidv 
 |-  ( ( ph /\ ( K e. LMod /\ K e. Ring ) ) -> ( A. r e. P A. z e. B A. w e. B ( ( ( r ( .s ` K ) z ) ( .r ` K ) w ) = ( r ( .s ` K ) ( z ( .r ` K ) w ) ) /\ ( z ( .r ` K ) ( r ( .s ` K ) w ) ) = ( r ( .s ` K ) ( z ( .r ` K ) w ) ) ) <-> A. r e. ( Base ` ( Scalar ` K ) ) A. z e. ( Base ` K ) A. w e. ( Base ` K ) ( ( ( r ( .s ` K ) z ) ( .r ` K ) w ) = ( r ( .s ` K ) ( z ( .r ` K ) w ) ) /\ ( z ( .r ` K ) ( r ( .s ` K ) w ) ) = ( r ( .s ` K ) ( z ( .r ` K ) w ) ) ) ) )
80 6 fveq2d 
 |-  ( ph -> ( Base ` F ) = ( Base ` ( Scalar ` L ) ) )
81 7 80 syl5eq 
 |-  ( ph -> P = ( Base ` ( Scalar ` L ) ) )
82 81 adantr 
 |-  ( ( ph /\ ( K e. LMod /\ K e. Ring ) ) -> P = ( Base ` ( Scalar ` L ) ) )
83 2 adantr 
 |-  ( ( ph /\ ( K e. LMod /\ K e. Ring ) ) -> B = ( Base ` L ) )
84 83 raleqdv 
 |-  ( ( ph /\ ( K e. LMod /\ K e. Ring ) ) -> ( A. w e. B ( ( ( r ( .s ` L ) z ) ( .r ` L ) w ) = ( r ( .s ` L ) ( z ( .r ` L ) w ) ) /\ ( z ( .r ` L ) ( r ( .s ` L ) w ) ) = ( r ( .s ` L ) ( z ( .r ` L ) w ) ) ) <-> A. w e. ( Base ` L ) ( ( ( r ( .s ` L ) z ) ( .r ` L ) w ) = ( r ( .s ` L ) ( z ( .r ` L ) w ) ) /\ ( z ( .r ` L ) ( r ( .s ` L ) w ) ) = ( r ( .s ` L ) ( z ( .r ` L ) w ) ) ) ) )
85 83 84 raleqbidv 
 |-  ( ( ph /\ ( K e. LMod /\ K e. Ring ) ) -> ( A. z e. B A. w e. B ( ( ( r ( .s ` L ) z ) ( .r ` L ) w ) = ( r ( .s ` L ) ( z ( .r ` L ) w ) ) /\ ( z ( .r ` L ) ( r ( .s ` L ) w ) ) = ( r ( .s ` L ) ( z ( .r ` L ) w ) ) ) <-> A. z e. ( Base ` L ) A. w e. ( Base ` L ) ( ( ( r ( .s ` L ) z ) ( .r ` L ) w ) = ( r ( .s ` L ) ( z ( .r ` L ) w ) ) /\ ( z ( .r ` L ) ( r ( .s ` L ) w ) ) = ( r ( .s ` L ) ( z ( .r ` L ) w ) ) ) ) )
86 82 85 raleqbidv 
 |-  ( ( ph /\ ( K e. LMod /\ K e. Ring ) ) -> ( A. r e. P A. z e. B A. w e. B ( ( ( r ( .s ` L ) z ) ( .r ` L ) w ) = ( r ( .s ` L ) ( z ( .r ` L ) w ) ) /\ ( z ( .r ` L ) ( r ( .s ` L ) w ) ) = ( r ( .s ` L ) ( z ( .r ` L ) w ) ) ) <-> A. r e. ( Base ` ( Scalar ` L ) ) A. z e. ( Base ` L ) A. w e. ( Base ` L ) ( ( ( r ( .s ` L ) z ) ( .r ` L ) w ) = ( r ( .s ` L ) ( z ( .r ` L ) w ) ) /\ ( z ( .r ` L ) ( r ( .s ` L ) w ) ) = ( r ( .s ` L ) ( z ( .r ` L ) w ) ) ) ) )
87 74 79 86 3bitr3d 
 |-  ( ( ph /\ ( K e. LMod /\ K e. Ring ) ) -> ( A. r e. ( Base ` ( Scalar ` K ) ) A. z e. ( Base ` K ) A. w e. ( Base ` K ) ( ( ( r ( .s ` K ) z ) ( .r ` K ) w ) = ( r ( .s ` K ) ( z ( .r ` K ) w ) ) /\ ( z ( .r ` K ) ( r ( .s ` K ) w ) ) = ( r ( .s ` K ) ( z ( .r ` K ) w ) ) ) <-> A. r e. ( Base ` ( Scalar ` L ) ) A. z e. ( Base ` L ) A. w e. ( Base ` L ) ( ( ( r ( .s ` L ) z ) ( .r ` L ) w ) = ( r ( .s ` L ) ( z ( .r ` L ) w ) ) /\ ( z ( .r ` L ) ( r ( .s ` L ) w ) ) = ( r ( .s ` L ) ( z ( .r ` L ) w ) ) ) ) )
88 23 87 anbi12d 
 |-  ( ( ph /\ ( K e. LMod /\ K e. Ring ) ) -> ( ( ( K e. LMod /\ K e. Ring /\ ( Scalar ` K ) e. CRing ) /\ A. r e. ( Base ` ( Scalar ` K ) ) A. z e. ( Base ` K ) A. w e. ( Base ` K ) ( ( ( r ( .s ` K ) z ) ( .r ` K ) w ) = ( r ( .s ` K ) ( z ( .r ` K ) w ) ) /\ ( z ( .r ` K ) ( r ( .s ` K ) w ) ) = ( r ( .s ` K ) ( z ( .r ` K ) w ) ) ) ) <-> ( ( L e. LMod /\ L e. Ring /\ ( Scalar ` L ) e. CRing ) /\ A. r e. ( Base ` ( Scalar ` L ) ) A. z e. ( Base ` L ) A. w e. ( Base ` L ) ( ( ( r ( .s ` L ) z ) ( .r ` L ) w ) = ( r ( .s ` L ) ( z ( .r ` L ) w ) ) /\ ( z ( .r ` L ) ( r ( .s ` L ) w ) ) = ( r ( .s ` L ) ( z ( .r ` L ) w ) ) ) ) ) )
89 34 35 37 36 50 isassa 
 |-  ( K e. AssAlg <-> ( ( K e. LMod /\ K e. Ring /\ ( Scalar ` K ) e. CRing ) /\ A. r e. ( Base ` ( Scalar ` K ) ) A. z e. ( Base ` K ) A. w e. ( Base ` K ) ( ( ( r ( .s ` K ) z ) ( .r ` K ) w ) = ( r ( .s ` K ) ( z ( .r ` K ) w ) ) /\ ( z ( .r ` K ) ( r ( .s ` K ) w ) ) = ( r ( .s ` K ) ( z ( .r ` K ) w ) ) ) ) )
90 eqid 
 |-  ( Base ` L ) = ( Base ` L )
91 eqid 
 |-  ( Scalar ` L ) = ( Scalar ` L )
92 eqid 
 |-  ( Base ` ( Scalar ` L ) ) = ( Base ` ( Scalar ` L ) )
93 eqid 
 |-  ( .s ` L ) = ( .s ` L )
94 eqid 
 |-  ( .r ` L ) = ( .r ` L )
95 90 91 92 93 94 isassa 
 |-  ( L e. AssAlg <-> ( ( L e. LMod /\ L e. Ring /\ ( Scalar ` L ) e. CRing ) /\ A. r e. ( Base ` ( Scalar ` L ) ) A. z e. ( Base ` L ) A. w e. ( Base ` L ) ( ( ( r ( .s ` L ) z ) ( .r ` L ) w ) = ( r ( .s ` L ) ( z ( .r ` L ) w ) ) /\ ( z ( .r ` L ) ( r ( .s ` L ) w ) ) = ( r ( .s ` L ) ( z ( .r ` L ) w ) ) ) ) )
96 88 89 95 3bitr4g 
 |-  ( ( ph /\ ( K e. LMod /\ K e. Ring ) ) -> ( K e. AssAlg <-> L e. AssAlg ) )
97 96 ex 
 |-  ( ph -> ( ( K e. LMod /\ K e. Ring ) -> ( K e. AssAlg <-> L e. AssAlg ) ) )
98 12 19 97 pm5.21ndd 
 |-  ( ph -> ( K e. AssAlg <-> L e. AssAlg ) )