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 imbitrrid
 |-  ( 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 imbitrrid
 |-  ( ph -> ( L e. AssAlg -> K e. Ring ) )
19 15 18 jcad
 |-  ( ph -> ( L e. AssAlg -> ( K e. LMod /\ K e. Ring ) ) )
20 14 17 anbi12d
 |-  ( ph -> ( ( K e. LMod /\ K e. Ring ) <-> ( L e. LMod /\ L e. Ring ) ) )
21 20 adantr
 |-  ( ( ph /\ ( K e. LMod /\ K e. Ring ) ) -> ( ( K e. LMod /\ K e. Ring ) <-> ( L e. LMod /\ L e. Ring ) ) )
22 simpll
 |-  ( ( ( ph /\ ( K e. LMod /\ K e. Ring ) ) /\ ( r e. P /\ ( z e. B /\ w e. B ) ) ) -> ph )
23 simplrl
 |-  ( ( ( ph /\ ( K e. LMod /\ K e. Ring ) ) /\ ( r e. P /\ ( z e. B /\ w e. B ) ) ) -> K e. LMod )
24 simprl
 |-  ( ( ( ph /\ ( K e. LMod /\ K e. Ring ) ) /\ ( r e. P /\ ( z e. B /\ w e. B ) ) ) -> r e. P )
25 5 fveq2d
 |-  ( ph -> ( Base ` F ) = ( Base ` ( Scalar ` K ) ) )
26 7 25 eqtrid
 |-  ( ph -> P = ( Base ` ( Scalar ` K ) ) )
27 22 26 syl
 |-  ( ( ( ph /\ ( K e. LMod /\ K e. Ring ) ) /\ ( r e. P /\ ( z e. B /\ w e. B ) ) ) -> P = ( Base ` ( Scalar ` K ) ) )
28 24 27 eleqtrd
 |-  ( ( ( ph /\ ( K e. LMod /\ K e. Ring ) ) /\ ( r e. P /\ ( z e. B /\ w e. B ) ) ) -> r e. ( Base ` ( Scalar ` K ) ) )
29 simprrl
 |-  ( ( ( ph /\ ( K e. LMod /\ K e. Ring ) ) /\ ( r e. P /\ ( z e. B /\ w e. B ) ) ) -> z e. B )
30 22 1 syl
 |-  ( ( ( ph /\ ( K e. LMod /\ K e. Ring ) ) /\ ( r e. P /\ ( z e. B /\ w e. B ) ) ) -> B = ( Base ` K ) )
31 29 30 eleqtrd
 |-  ( ( ( ph /\ ( K e. LMod /\ K e. Ring ) ) /\ ( r e. P /\ ( z e. B /\ w e. B ) ) ) -> z e. ( Base ` K ) )
32 eqid
 |-  ( Base ` K ) = ( Base ` K )
33 eqid
 |-  ( Scalar ` K ) = ( Scalar ` K )
34 eqid
 |-  ( .s ` K ) = ( .s ` K )
35 eqid
 |-  ( Base ` ( Scalar ` K ) ) = ( Base ` ( Scalar ` K ) )
36 32 33 34 35 lmodvscl
 |-  ( ( K e. LMod /\ r e. ( Base ` ( Scalar ` K ) ) /\ z e. ( Base ` K ) ) -> ( r ( .s ` K ) z ) e. ( Base ` K ) )
37 23 28 31 36 syl3anc
 |-  ( ( ( ph /\ ( K e. LMod /\ K e. Ring ) ) /\ ( r e. P /\ ( z e. B /\ w e. B ) ) ) -> ( r ( .s ` K ) z ) e. ( Base ` K ) )
38 37 30 eleqtrrd
 |-  ( ( ( ph /\ ( K e. LMod /\ K e. Ring ) ) /\ ( r e. P /\ ( z e. B /\ w e. B ) ) ) -> ( r ( .s ` K ) z ) e. B )
39 simprrr
 |-  ( ( ( ph /\ ( K e. LMod /\ K e. Ring ) ) /\ ( r e. P /\ ( z e. B /\ w e. B ) ) ) -> w e. B )
40 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 ) )
41 22 38 39 40 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 ) )
42 8 oveqrspc2v
 |-  ( ( ph /\ ( r e. P /\ z e. B ) ) -> ( r ( .s ` K ) z ) = ( r ( .s ` L ) z ) )
43 22 24 29 42 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 ) )
44 43 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 ) )
45 41 44 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 ) )
46 eqid
 |-  ( .r ` K ) = ( .r ` K )
47 simplrr
 |-  ( ( ( ph /\ ( K e. LMod /\ K e. Ring ) ) /\ ( r e. P /\ ( z e. B /\ w e. B ) ) ) -> K e. Ring )
48 39 30 eleqtrd
 |-  ( ( ( ph /\ ( K e. LMod /\ K e. Ring ) ) /\ ( r e. P /\ ( z e. B /\ w e. B ) ) ) -> w e. ( Base ` K ) )
49 32 46 47 31 48 ringcld
 |-  ( ( ( ph /\ ( K e. LMod /\ K e. Ring ) ) /\ ( r e. P /\ ( z e. B /\ w e. B ) ) ) -> ( z ( .r ` K ) w ) e. ( Base ` K ) )
50 49 30 eleqtrrd
 |-  ( ( ( ph /\ ( K e. LMod /\ K e. Ring ) ) /\ ( r e. P /\ ( z e. B /\ w e. B ) ) ) -> ( z ( .r ` K ) w ) e. B )
51 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 ) ) )
52 22 24 50 51 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 ) ) )
53 4 oveqrspc2v
 |-  ( ( ph /\ ( z e. B /\ w e. B ) ) -> ( z ( .r ` K ) w ) = ( z ( .r ` L ) w ) )
54 22 29 39 53 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 ) )
55 54 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 ) ) )
56 52 55 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 ) ) )
57 45 56 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 ) ) ) )
58 32 33 34 35 lmodvscl
 |-  ( ( K e. LMod /\ r e. ( Base ` ( Scalar ` K ) ) /\ w e. ( Base ` K ) ) -> ( r ( .s ` K ) w ) e. ( Base ` K ) )
59 23 28 48 58 syl3anc
 |-  ( ( ( ph /\ ( K e. LMod /\ K e. Ring ) ) /\ ( r e. P /\ ( z e. B /\ w e. B ) ) ) -> ( r ( .s ` K ) w ) e. ( Base ` K ) )
60 59 30 eleqtrrd
 |-  ( ( ( ph /\ ( K e. LMod /\ K e. Ring ) ) /\ ( r e. P /\ ( z e. B /\ w e. B ) ) ) -> ( r ( .s ` K ) w ) e. B )
61 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 ) ) )
62 22 29 60 61 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 ) ) )
63 8 oveqrspc2v
 |-  ( ( ph /\ ( r e. P /\ w e. B ) ) -> ( r ( .s ` K ) w ) = ( r ( .s ` L ) w ) )
64 22 24 39 63 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 ) )
65 64 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 ) ) )
66 62 65 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 ) ) )
67 66 56 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 ) ) ) )
68 57 67 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 ) ) ) ) )
69 68 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 ) ) ) ) )
70 69 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 ) ) ) ) )
71 70 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 ) ) ) ) )
72 26 adantr
 |-  ( ( ph /\ ( K e. LMod /\ K e. Ring ) ) -> P = ( Base ` ( Scalar ` K ) ) )
73 1 adantr
 |-  ( ( ph /\ ( K e. LMod /\ K e. Ring ) ) -> B = ( Base ` K ) )
74 73 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 ) ) ) ) )
75 73 74 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 ) ) ) ) )
76 72 75 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 ) ) ) ) )
77 6 fveq2d
 |-  ( ph -> ( Base ` F ) = ( Base ` ( Scalar ` L ) ) )
78 7 77 eqtrid
 |-  ( ph -> P = ( Base ` ( Scalar ` L ) ) )
79 78 adantr
 |-  ( ( ph /\ ( K e. LMod /\ K e. Ring ) ) -> P = ( Base ` ( Scalar ` L ) ) )
80 2 adantr
 |-  ( ( ph /\ ( K e. LMod /\ K e. Ring ) ) -> B = ( Base ` L ) )
81 80 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 ) ) ) ) )
82 80 81 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 ) ) ) ) )
83 79 82 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 ) ) ) ) )
84 71 76 83 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 ) ) ) ) )
85 21 84 anbi12d
 |-  ( ( ph /\ ( K e. LMod /\ K e. Ring ) ) -> ( ( ( 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 ) ) ) ) <-> ( ( L e. LMod /\ L e. Ring ) /\ 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 ) ) ) ) ) )
86 32 33 35 34 46 isassa
 |-  ( K e. AssAlg <-> ( ( 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 ) ) ) ) )
87 eqid
 |-  ( Base ` L ) = ( Base ` L )
88 eqid
 |-  ( Scalar ` L ) = ( Scalar ` L )
89 eqid
 |-  ( Base ` ( Scalar ` L ) ) = ( Base ` ( Scalar ` L ) )
90 eqid
 |-  ( .s ` L ) = ( .s ` L )
91 eqid
 |-  ( .r ` L ) = ( .r ` L )
92 87 88 89 90 91 isassa
 |-  ( L e. AssAlg <-> ( ( L e. LMod /\ L e. Ring ) /\ 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 ) ) ) ) )
93 85 86 92 3bitr4g
 |-  ( ( ph /\ ( K e. LMod /\ K e. Ring ) ) -> ( K e. AssAlg <-> L e. AssAlg ) )
94 93 ex
 |-  ( ph -> ( ( K e. LMod /\ K e. Ring ) -> ( K e. AssAlg <-> L e. AssAlg ) ) )
95 12 19 94 pm5.21ndd
 |-  ( ph -> ( K e. AssAlg <-> L e. AssAlg ) )