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 ) ) |