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 ( 𝜑𝐵 = ( Base ‘ 𝐾 ) )
assapropd.2 ( 𝜑𝐵 = ( Base ‘ 𝐿 ) )
assapropd.3 ( ( 𝜑 ∧ ( 𝑥𝐵𝑦𝐵 ) ) → ( 𝑥 ( +g𝐾 ) 𝑦 ) = ( 𝑥 ( +g𝐿 ) 𝑦 ) )
assapropd.4 ( ( 𝜑 ∧ ( 𝑥𝐵𝑦𝐵 ) ) → ( 𝑥 ( .r𝐾 ) 𝑦 ) = ( 𝑥 ( .r𝐿 ) 𝑦 ) )
assapropd.5 ( 𝜑𝐹 = ( Scalar ‘ 𝐾 ) )
assapropd.6 ( 𝜑𝐹 = ( Scalar ‘ 𝐿 ) )
assapropd.7 𝑃 = ( Base ‘ 𝐹 )
assapropd.8 ( ( 𝜑 ∧ ( 𝑥𝑃𝑦𝐵 ) ) → ( 𝑥 ( ·𝑠𝐾 ) 𝑦 ) = ( 𝑥 ( ·𝑠𝐿 ) 𝑦 ) )
Assertion assapropd ( 𝜑 → ( 𝐾 ∈ AssAlg ↔ 𝐿 ∈ AssAlg ) )

Proof

Step Hyp Ref Expression
1 assapropd.1 ( 𝜑𝐵 = ( Base ‘ 𝐾 ) )
2 assapropd.2 ( 𝜑𝐵 = ( Base ‘ 𝐿 ) )
3 assapropd.3 ( ( 𝜑 ∧ ( 𝑥𝐵𝑦𝐵 ) ) → ( 𝑥 ( +g𝐾 ) 𝑦 ) = ( 𝑥 ( +g𝐿 ) 𝑦 ) )
4 assapropd.4 ( ( 𝜑 ∧ ( 𝑥𝐵𝑦𝐵 ) ) → ( 𝑥 ( .r𝐾 ) 𝑦 ) = ( 𝑥 ( .r𝐿 ) 𝑦 ) )
5 assapropd.5 ( 𝜑𝐹 = ( Scalar ‘ 𝐾 ) )
6 assapropd.6 ( 𝜑𝐹 = ( Scalar ‘ 𝐿 ) )
7 assapropd.7 𝑃 = ( Base ‘ 𝐹 )
8 assapropd.8 ( ( 𝜑 ∧ ( 𝑥𝑃𝑦𝐵 ) ) → ( 𝑥 ( ·𝑠𝐾 ) 𝑦 ) = ( 𝑥 ( ·𝑠𝐿 ) 𝑦 ) )
9 assalmod ( 𝐾 ∈ AssAlg → 𝐾 ∈ LMod )
10 assaring ( 𝐾 ∈ AssAlg → 𝐾 ∈ Ring )
11 9 10 jca ( 𝐾 ∈ AssAlg → ( 𝐾 ∈ LMod ∧ 𝐾 ∈ Ring ) )
12 11 a1i ( 𝜑 → ( 𝐾 ∈ AssAlg → ( 𝐾 ∈ LMod ∧ 𝐾 ∈ Ring ) ) )
13 assalmod ( 𝐿 ∈ AssAlg → 𝐿 ∈ LMod )
14 1 2 3 5 6 7 8 lmodpropd ( 𝜑 → ( 𝐾 ∈ LMod ↔ 𝐿 ∈ LMod ) )
15 13 14 imbitrrid ( 𝜑 → ( 𝐿 ∈ AssAlg → 𝐾 ∈ LMod ) )
16 assaring ( 𝐿 ∈ AssAlg → 𝐿 ∈ Ring )
17 1 2 3 4 ringpropd ( 𝜑 → ( 𝐾 ∈ Ring ↔ 𝐿 ∈ Ring ) )
18 16 17 imbitrrid ( 𝜑 → ( 𝐿 ∈ AssAlg → 𝐾 ∈ Ring ) )
19 15 18 jcad ( 𝜑 → ( 𝐿 ∈ AssAlg → ( 𝐾 ∈ LMod ∧ 𝐾 ∈ Ring ) ) )
20 14 17 anbi12d ( 𝜑 → ( ( 𝐾 ∈ LMod ∧ 𝐾 ∈ Ring ) ↔ ( 𝐿 ∈ LMod ∧ 𝐿 ∈ Ring ) ) )
21 20 adantr ( ( 𝜑 ∧ ( 𝐾 ∈ LMod ∧ 𝐾 ∈ Ring ) ) → ( ( 𝐾 ∈ LMod ∧ 𝐾 ∈ Ring ) ↔ ( 𝐿 ∈ LMod ∧ 𝐿 ∈ Ring ) ) )
22 simpll ( ( ( 𝜑 ∧ ( 𝐾 ∈ LMod ∧ 𝐾 ∈ Ring ) ) ∧ ( 𝑟𝑃 ∧ ( 𝑧𝐵𝑤𝐵 ) ) ) → 𝜑 )
23 simplrl ( ( ( 𝜑 ∧ ( 𝐾 ∈ LMod ∧ 𝐾 ∈ Ring ) ) ∧ ( 𝑟𝑃 ∧ ( 𝑧𝐵𝑤𝐵 ) ) ) → 𝐾 ∈ LMod )
24 simprl ( ( ( 𝜑 ∧ ( 𝐾 ∈ LMod ∧ 𝐾 ∈ Ring ) ) ∧ ( 𝑟𝑃 ∧ ( 𝑧𝐵𝑤𝐵 ) ) ) → 𝑟𝑃 )
25 5 fveq2d ( 𝜑 → ( Base ‘ 𝐹 ) = ( Base ‘ ( Scalar ‘ 𝐾 ) ) )
26 7 25 eqtrid ( 𝜑𝑃 = ( Base ‘ ( Scalar ‘ 𝐾 ) ) )
27 22 26 syl ( ( ( 𝜑 ∧ ( 𝐾 ∈ LMod ∧ 𝐾 ∈ Ring ) ) ∧ ( 𝑟𝑃 ∧ ( 𝑧𝐵𝑤𝐵 ) ) ) → 𝑃 = ( Base ‘ ( Scalar ‘ 𝐾 ) ) )
28 24 27 eleqtrd ( ( ( 𝜑 ∧ ( 𝐾 ∈ LMod ∧ 𝐾 ∈ Ring ) ) ∧ ( 𝑟𝑃 ∧ ( 𝑧𝐵𝑤𝐵 ) ) ) → 𝑟 ∈ ( Base ‘ ( Scalar ‘ 𝐾 ) ) )
29 simprrl ( ( ( 𝜑 ∧ ( 𝐾 ∈ LMod ∧ 𝐾 ∈ Ring ) ) ∧ ( 𝑟𝑃 ∧ ( 𝑧𝐵𝑤𝐵 ) ) ) → 𝑧𝐵 )
30 22 1 syl ( ( ( 𝜑 ∧ ( 𝐾 ∈ LMod ∧ 𝐾 ∈ Ring ) ) ∧ ( 𝑟𝑃 ∧ ( 𝑧𝐵𝑤𝐵 ) ) ) → 𝐵 = ( Base ‘ 𝐾 ) )
31 29 30 eleqtrd ( ( ( 𝜑 ∧ ( 𝐾 ∈ LMod ∧ 𝐾 ∈ Ring ) ) ∧ ( 𝑟𝑃 ∧ ( 𝑧𝐵𝑤𝐵 ) ) ) → 𝑧 ∈ ( Base ‘ 𝐾 ) )
32 eqid ( Base ‘ 𝐾 ) = ( Base ‘ 𝐾 )
33 eqid ( Scalar ‘ 𝐾 ) = ( Scalar ‘ 𝐾 )
34 eqid ( ·𝑠𝐾 ) = ( ·𝑠𝐾 )
35 eqid ( Base ‘ ( Scalar ‘ 𝐾 ) ) = ( Base ‘ ( Scalar ‘ 𝐾 ) )
36 32 33 34 35 lmodvscl ( ( 𝐾 ∈ LMod ∧ 𝑟 ∈ ( Base ‘ ( Scalar ‘ 𝐾 ) ) ∧ 𝑧 ∈ ( Base ‘ 𝐾 ) ) → ( 𝑟 ( ·𝑠𝐾 ) 𝑧 ) ∈ ( Base ‘ 𝐾 ) )
37 23 28 31 36 syl3anc ( ( ( 𝜑 ∧ ( 𝐾 ∈ LMod ∧ 𝐾 ∈ Ring ) ) ∧ ( 𝑟𝑃 ∧ ( 𝑧𝐵𝑤𝐵 ) ) ) → ( 𝑟 ( ·𝑠𝐾 ) 𝑧 ) ∈ ( Base ‘ 𝐾 ) )
38 37 30 eleqtrrd ( ( ( 𝜑 ∧ ( 𝐾 ∈ LMod ∧ 𝐾 ∈ Ring ) ) ∧ ( 𝑟𝑃 ∧ ( 𝑧𝐵𝑤𝐵 ) ) ) → ( 𝑟 ( ·𝑠𝐾 ) 𝑧 ) ∈ 𝐵 )
39 simprrr ( ( ( 𝜑 ∧ ( 𝐾 ∈ LMod ∧ 𝐾 ∈ Ring ) ) ∧ ( 𝑟𝑃 ∧ ( 𝑧𝐵𝑤𝐵 ) ) ) → 𝑤𝐵 )
40 4 oveqrspc2v ( ( 𝜑 ∧ ( ( 𝑟 ( ·𝑠𝐾 ) 𝑧 ) ∈ 𝐵𝑤𝐵 ) ) → ( ( 𝑟 ( ·𝑠𝐾 ) 𝑧 ) ( .r𝐾 ) 𝑤 ) = ( ( 𝑟 ( ·𝑠𝐾 ) 𝑧 ) ( .r𝐿 ) 𝑤 ) )
41 22 38 39 40 syl12anc ( ( ( 𝜑 ∧ ( 𝐾 ∈ LMod ∧ 𝐾 ∈ Ring ) ) ∧ ( 𝑟𝑃 ∧ ( 𝑧𝐵𝑤𝐵 ) ) ) → ( ( 𝑟 ( ·𝑠𝐾 ) 𝑧 ) ( .r𝐾 ) 𝑤 ) = ( ( 𝑟 ( ·𝑠𝐾 ) 𝑧 ) ( .r𝐿 ) 𝑤 ) )
42 8 oveqrspc2v ( ( 𝜑 ∧ ( 𝑟𝑃𝑧𝐵 ) ) → ( 𝑟 ( ·𝑠𝐾 ) 𝑧 ) = ( 𝑟 ( ·𝑠𝐿 ) 𝑧 ) )
43 22 24 29 42 syl12anc ( ( ( 𝜑 ∧ ( 𝐾 ∈ LMod ∧ 𝐾 ∈ Ring ) ) ∧ ( 𝑟𝑃 ∧ ( 𝑧𝐵𝑤𝐵 ) ) ) → ( 𝑟 ( ·𝑠𝐾 ) 𝑧 ) = ( 𝑟 ( ·𝑠𝐿 ) 𝑧 ) )
44 43 oveq1d ( ( ( 𝜑 ∧ ( 𝐾 ∈ LMod ∧ 𝐾 ∈ Ring ) ) ∧ ( 𝑟𝑃 ∧ ( 𝑧𝐵𝑤𝐵 ) ) ) → ( ( 𝑟 ( ·𝑠𝐾 ) 𝑧 ) ( .r𝐿 ) 𝑤 ) = ( ( 𝑟 ( ·𝑠𝐿 ) 𝑧 ) ( .r𝐿 ) 𝑤 ) )
45 41 44 eqtrd ( ( ( 𝜑 ∧ ( 𝐾 ∈ LMod ∧ 𝐾 ∈ Ring ) ) ∧ ( 𝑟𝑃 ∧ ( 𝑧𝐵𝑤𝐵 ) ) ) → ( ( 𝑟 ( ·𝑠𝐾 ) 𝑧 ) ( .r𝐾 ) 𝑤 ) = ( ( 𝑟 ( ·𝑠𝐿 ) 𝑧 ) ( .r𝐿 ) 𝑤 ) )
46 eqid ( .r𝐾 ) = ( .r𝐾 )
47 simplrr ( ( ( 𝜑 ∧ ( 𝐾 ∈ LMod ∧ 𝐾 ∈ Ring ) ) ∧ ( 𝑟𝑃 ∧ ( 𝑧𝐵𝑤𝐵 ) ) ) → 𝐾 ∈ Ring )
48 39 30 eleqtrd ( ( ( 𝜑 ∧ ( 𝐾 ∈ LMod ∧ 𝐾 ∈ Ring ) ) ∧ ( 𝑟𝑃 ∧ ( 𝑧𝐵𝑤𝐵 ) ) ) → 𝑤 ∈ ( Base ‘ 𝐾 ) )
49 32 46 47 31 48 ringcld ( ( ( 𝜑 ∧ ( 𝐾 ∈ LMod ∧ 𝐾 ∈ Ring ) ) ∧ ( 𝑟𝑃 ∧ ( 𝑧𝐵𝑤𝐵 ) ) ) → ( 𝑧 ( .r𝐾 ) 𝑤 ) ∈ ( Base ‘ 𝐾 ) )
50 49 30 eleqtrrd ( ( ( 𝜑 ∧ ( 𝐾 ∈ LMod ∧ 𝐾 ∈ Ring ) ) ∧ ( 𝑟𝑃 ∧ ( 𝑧𝐵𝑤𝐵 ) ) ) → ( 𝑧 ( .r𝐾 ) 𝑤 ) ∈ 𝐵 )
51 8 oveqrspc2v ( ( 𝜑 ∧ ( 𝑟𝑃 ∧ ( 𝑧 ( .r𝐾 ) 𝑤 ) ∈ 𝐵 ) ) → ( 𝑟 ( ·𝑠𝐾 ) ( 𝑧 ( .r𝐾 ) 𝑤 ) ) = ( 𝑟 ( ·𝑠𝐿 ) ( 𝑧 ( .r𝐾 ) 𝑤 ) ) )
52 22 24 50 51 syl12anc ( ( ( 𝜑 ∧ ( 𝐾 ∈ LMod ∧ 𝐾 ∈ Ring ) ) ∧ ( 𝑟𝑃 ∧ ( 𝑧𝐵𝑤𝐵 ) ) ) → ( 𝑟 ( ·𝑠𝐾 ) ( 𝑧 ( .r𝐾 ) 𝑤 ) ) = ( 𝑟 ( ·𝑠𝐿 ) ( 𝑧 ( .r𝐾 ) 𝑤 ) ) )
53 4 oveqrspc2v ( ( 𝜑 ∧ ( 𝑧𝐵𝑤𝐵 ) ) → ( 𝑧 ( .r𝐾 ) 𝑤 ) = ( 𝑧 ( .r𝐿 ) 𝑤 ) )
54 22 29 39 53 syl12anc ( ( ( 𝜑 ∧ ( 𝐾 ∈ LMod ∧ 𝐾 ∈ Ring ) ) ∧ ( 𝑟𝑃 ∧ ( 𝑧𝐵𝑤𝐵 ) ) ) → ( 𝑧 ( .r𝐾 ) 𝑤 ) = ( 𝑧 ( .r𝐿 ) 𝑤 ) )
55 54 oveq2d ( ( ( 𝜑 ∧ ( 𝐾 ∈ LMod ∧ 𝐾 ∈ Ring ) ) ∧ ( 𝑟𝑃 ∧ ( 𝑧𝐵𝑤𝐵 ) ) ) → ( 𝑟 ( ·𝑠𝐿 ) ( 𝑧 ( .r𝐾 ) 𝑤 ) ) = ( 𝑟 ( ·𝑠𝐿 ) ( 𝑧 ( .r𝐿 ) 𝑤 ) ) )
56 52 55 eqtrd ( ( ( 𝜑 ∧ ( 𝐾 ∈ LMod ∧ 𝐾 ∈ Ring ) ) ∧ ( 𝑟𝑃 ∧ ( 𝑧𝐵𝑤𝐵 ) ) ) → ( 𝑟 ( ·𝑠𝐾 ) ( 𝑧 ( .r𝐾 ) 𝑤 ) ) = ( 𝑟 ( ·𝑠𝐿 ) ( 𝑧 ( .r𝐿 ) 𝑤 ) ) )
57 45 56 eqeq12d ( ( ( 𝜑 ∧ ( 𝐾 ∈ LMod ∧ 𝐾 ∈ Ring ) ) ∧ ( 𝑟𝑃 ∧ ( 𝑧𝐵𝑤𝐵 ) ) ) → ( ( ( 𝑟 ( ·𝑠𝐾 ) 𝑧 ) ( .r𝐾 ) 𝑤 ) = ( 𝑟 ( ·𝑠𝐾 ) ( 𝑧 ( .r𝐾 ) 𝑤 ) ) ↔ ( ( 𝑟 ( ·𝑠𝐿 ) 𝑧 ) ( .r𝐿 ) 𝑤 ) = ( 𝑟 ( ·𝑠𝐿 ) ( 𝑧 ( .r𝐿 ) 𝑤 ) ) ) )
58 32 33 34 35 lmodvscl ( ( 𝐾 ∈ LMod ∧ 𝑟 ∈ ( Base ‘ ( Scalar ‘ 𝐾 ) ) ∧ 𝑤 ∈ ( Base ‘ 𝐾 ) ) → ( 𝑟 ( ·𝑠𝐾 ) 𝑤 ) ∈ ( Base ‘ 𝐾 ) )
59 23 28 48 58 syl3anc ( ( ( 𝜑 ∧ ( 𝐾 ∈ LMod ∧ 𝐾 ∈ Ring ) ) ∧ ( 𝑟𝑃 ∧ ( 𝑧𝐵𝑤𝐵 ) ) ) → ( 𝑟 ( ·𝑠𝐾 ) 𝑤 ) ∈ ( Base ‘ 𝐾 ) )
60 59 30 eleqtrrd ( ( ( 𝜑 ∧ ( 𝐾 ∈ LMod ∧ 𝐾 ∈ Ring ) ) ∧ ( 𝑟𝑃 ∧ ( 𝑧𝐵𝑤𝐵 ) ) ) → ( 𝑟 ( ·𝑠𝐾 ) 𝑤 ) ∈ 𝐵 )
61 4 oveqrspc2v ( ( 𝜑 ∧ ( 𝑧𝐵 ∧ ( 𝑟 ( ·𝑠𝐾 ) 𝑤 ) ∈ 𝐵 ) ) → ( 𝑧 ( .r𝐾 ) ( 𝑟 ( ·𝑠𝐾 ) 𝑤 ) ) = ( 𝑧 ( .r𝐿 ) ( 𝑟 ( ·𝑠𝐾 ) 𝑤 ) ) )
62 22 29 60 61 syl12anc ( ( ( 𝜑 ∧ ( 𝐾 ∈ LMod ∧ 𝐾 ∈ Ring ) ) ∧ ( 𝑟𝑃 ∧ ( 𝑧𝐵𝑤𝐵 ) ) ) → ( 𝑧 ( .r𝐾 ) ( 𝑟 ( ·𝑠𝐾 ) 𝑤 ) ) = ( 𝑧 ( .r𝐿 ) ( 𝑟 ( ·𝑠𝐾 ) 𝑤 ) ) )
63 8 oveqrspc2v ( ( 𝜑 ∧ ( 𝑟𝑃𝑤𝐵 ) ) → ( 𝑟 ( ·𝑠𝐾 ) 𝑤 ) = ( 𝑟 ( ·𝑠𝐿 ) 𝑤 ) )
64 22 24 39 63 syl12anc ( ( ( 𝜑 ∧ ( 𝐾 ∈ LMod ∧ 𝐾 ∈ Ring ) ) ∧ ( 𝑟𝑃 ∧ ( 𝑧𝐵𝑤𝐵 ) ) ) → ( 𝑟 ( ·𝑠𝐾 ) 𝑤 ) = ( 𝑟 ( ·𝑠𝐿 ) 𝑤 ) )
65 64 oveq2d ( ( ( 𝜑 ∧ ( 𝐾 ∈ LMod ∧ 𝐾 ∈ Ring ) ) ∧ ( 𝑟𝑃 ∧ ( 𝑧𝐵𝑤𝐵 ) ) ) → ( 𝑧 ( .r𝐿 ) ( 𝑟 ( ·𝑠𝐾 ) 𝑤 ) ) = ( 𝑧 ( .r𝐿 ) ( 𝑟 ( ·𝑠𝐿 ) 𝑤 ) ) )
66 62 65 eqtrd ( ( ( 𝜑 ∧ ( 𝐾 ∈ LMod ∧ 𝐾 ∈ Ring ) ) ∧ ( 𝑟𝑃 ∧ ( 𝑧𝐵𝑤𝐵 ) ) ) → ( 𝑧 ( .r𝐾 ) ( 𝑟 ( ·𝑠𝐾 ) 𝑤 ) ) = ( 𝑧 ( .r𝐿 ) ( 𝑟 ( ·𝑠𝐿 ) 𝑤 ) ) )
67 66 56 eqeq12d ( ( ( 𝜑 ∧ ( 𝐾 ∈ LMod ∧ 𝐾 ∈ Ring ) ) ∧ ( 𝑟𝑃 ∧ ( 𝑧𝐵𝑤𝐵 ) ) ) → ( ( 𝑧 ( .r𝐾 ) ( 𝑟 ( ·𝑠𝐾 ) 𝑤 ) ) = ( 𝑟 ( ·𝑠𝐾 ) ( 𝑧 ( .r𝐾 ) 𝑤 ) ) ↔ ( 𝑧 ( .r𝐿 ) ( 𝑟 ( ·𝑠𝐿 ) 𝑤 ) ) = ( 𝑟 ( ·𝑠𝐿 ) ( 𝑧 ( .r𝐿 ) 𝑤 ) ) ) )
68 57 67 anbi12d ( ( ( 𝜑 ∧ ( 𝐾 ∈ LMod ∧ 𝐾 ∈ Ring ) ) ∧ ( 𝑟𝑃 ∧ ( 𝑧𝐵𝑤𝐵 ) ) ) → ( ( ( ( 𝑟 ( ·𝑠𝐾 ) 𝑧 ) ( .r𝐾 ) 𝑤 ) = ( 𝑟 ( ·𝑠𝐾 ) ( 𝑧 ( .r𝐾 ) 𝑤 ) ) ∧ ( 𝑧 ( .r𝐾 ) ( 𝑟 ( ·𝑠𝐾 ) 𝑤 ) ) = ( 𝑟 ( ·𝑠𝐾 ) ( 𝑧 ( .r𝐾 ) 𝑤 ) ) ) ↔ ( ( ( 𝑟 ( ·𝑠𝐿 ) 𝑧 ) ( .r𝐿 ) 𝑤 ) = ( 𝑟 ( ·𝑠𝐿 ) ( 𝑧 ( .r𝐿 ) 𝑤 ) ) ∧ ( 𝑧 ( .r𝐿 ) ( 𝑟 ( ·𝑠𝐿 ) 𝑤 ) ) = ( 𝑟 ( ·𝑠𝐿 ) ( 𝑧 ( .r𝐿 ) 𝑤 ) ) ) ) )
69 68 anassrs ( ( ( ( 𝜑 ∧ ( 𝐾 ∈ LMod ∧ 𝐾 ∈ Ring ) ) ∧ 𝑟𝑃 ) ∧ ( 𝑧𝐵𝑤𝐵 ) ) → ( ( ( ( 𝑟 ( ·𝑠𝐾 ) 𝑧 ) ( .r𝐾 ) 𝑤 ) = ( 𝑟 ( ·𝑠𝐾 ) ( 𝑧 ( .r𝐾 ) 𝑤 ) ) ∧ ( 𝑧 ( .r𝐾 ) ( 𝑟 ( ·𝑠𝐾 ) 𝑤 ) ) = ( 𝑟 ( ·𝑠𝐾 ) ( 𝑧 ( .r𝐾 ) 𝑤 ) ) ) ↔ ( ( ( 𝑟 ( ·𝑠𝐿 ) 𝑧 ) ( .r𝐿 ) 𝑤 ) = ( 𝑟 ( ·𝑠𝐿 ) ( 𝑧 ( .r𝐿 ) 𝑤 ) ) ∧ ( 𝑧 ( .r𝐿 ) ( 𝑟 ( ·𝑠𝐿 ) 𝑤 ) ) = ( 𝑟 ( ·𝑠𝐿 ) ( 𝑧 ( .r𝐿 ) 𝑤 ) ) ) ) )
70 69 2ralbidva ( ( ( 𝜑 ∧ ( 𝐾 ∈ LMod ∧ 𝐾 ∈ Ring ) ) ∧ 𝑟𝑃 ) → ( ∀ 𝑧𝐵𝑤𝐵 ( ( ( 𝑟 ( ·𝑠𝐾 ) 𝑧 ) ( .r𝐾 ) 𝑤 ) = ( 𝑟 ( ·𝑠𝐾 ) ( 𝑧 ( .r𝐾 ) 𝑤 ) ) ∧ ( 𝑧 ( .r𝐾 ) ( 𝑟 ( ·𝑠𝐾 ) 𝑤 ) ) = ( 𝑟 ( ·𝑠𝐾 ) ( 𝑧 ( .r𝐾 ) 𝑤 ) ) ) ↔ ∀ 𝑧𝐵𝑤𝐵 ( ( ( 𝑟 ( ·𝑠𝐿 ) 𝑧 ) ( .r𝐿 ) 𝑤 ) = ( 𝑟 ( ·𝑠𝐿 ) ( 𝑧 ( .r𝐿 ) 𝑤 ) ) ∧ ( 𝑧 ( .r𝐿 ) ( 𝑟 ( ·𝑠𝐿 ) 𝑤 ) ) = ( 𝑟 ( ·𝑠𝐿 ) ( 𝑧 ( .r𝐿 ) 𝑤 ) ) ) ) )
71 70 ralbidva ( ( 𝜑 ∧ ( 𝐾 ∈ LMod ∧ 𝐾 ∈ Ring ) ) → ( ∀ 𝑟𝑃𝑧𝐵𝑤𝐵 ( ( ( 𝑟 ( ·𝑠𝐾 ) 𝑧 ) ( .r𝐾 ) 𝑤 ) = ( 𝑟 ( ·𝑠𝐾 ) ( 𝑧 ( .r𝐾 ) 𝑤 ) ) ∧ ( 𝑧 ( .r𝐾 ) ( 𝑟 ( ·𝑠𝐾 ) 𝑤 ) ) = ( 𝑟 ( ·𝑠𝐾 ) ( 𝑧 ( .r𝐾 ) 𝑤 ) ) ) ↔ ∀ 𝑟𝑃𝑧𝐵𝑤𝐵 ( ( ( 𝑟 ( ·𝑠𝐿 ) 𝑧 ) ( .r𝐿 ) 𝑤 ) = ( 𝑟 ( ·𝑠𝐿 ) ( 𝑧 ( .r𝐿 ) 𝑤 ) ) ∧ ( 𝑧 ( .r𝐿 ) ( 𝑟 ( ·𝑠𝐿 ) 𝑤 ) ) = ( 𝑟 ( ·𝑠𝐿 ) ( 𝑧 ( .r𝐿 ) 𝑤 ) ) ) ) )
72 26 adantr ( ( 𝜑 ∧ ( 𝐾 ∈ LMod ∧ 𝐾 ∈ Ring ) ) → 𝑃 = ( Base ‘ ( Scalar ‘ 𝐾 ) ) )
73 1 adantr ( ( 𝜑 ∧ ( 𝐾 ∈ LMod ∧ 𝐾 ∈ Ring ) ) → 𝐵 = ( Base ‘ 𝐾 ) )
74 73 raleqdv ( ( 𝜑 ∧ ( 𝐾 ∈ LMod ∧ 𝐾 ∈ Ring ) ) → ( ∀ 𝑤𝐵 ( ( ( 𝑟 ( ·𝑠𝐾 ) 𝑧 ) ( .r𝐾 ) 𝑤 ) = ( 𝑟 ( ·𝑠𝐾 ) ( 𝑧 ( .r𝐾 ) 𝑤 ) ) ∧ ( 𝑧 ( .r𝐾 ) ( 𝑟 ( ·𝑠𝐾 ) 𝑤 ) ) = ( 𝑟 ( ·𝑠𝐾 ) ( 𝑧 ( .r𝐾 ) 𝑤 ) ) ) ↔ ∀ 𝑤 ∈ ( Base ‘ 𝐾 ) ( ( ( 𝑟 ( ·𝑠𝐾 ) 𝑧 ) ( .r𝐾 ) 𝑤 ) = ( 𝑟 ( ·𝑠𝐾 ) ( 𝑧 ( .r𝐾 ) 𝑤 ) ) ∧ ( 𝑧 ( .r𝐾 ) ( 𝑟 ( ·𝑠𝐾 ) 𝑤 ) ) = ( 𝑟 ( ·𝑠𝐾 ) ( 𝑧 ( .r𝐾 ) 𝑤 ) ) ) ) )
75 73 74 raleqbidv ( ( 𝜑 ∧ ( 𝐾 ∈ LMod ∧ 𝐾 ∈ Ring ) ) → ( ∀ 𝑧𝐵𝑤𝐵 ( ( ( 𝑟 ( ·𝑠𝐾 ) 𝑧 ) ( .r𝐾 ) 𝑤 ) = ( 𝑟 ( ·𝑠𝐾 ) ( 𝑧 ( .r𝐾 ) 𝑤 ) ) ∧ ( 𝑧 ( .r𝐾 ) ( 𝑟 ( ·𝑠𝐾 ) 𝑤 ) ) = ( 𝑟 ( ·𝑠𝐾 ) ( 𝑧 ( .r𝐾 ) 𝑤 ) ) ) ↔ ∀ 𝑧 ∈ ( Base ‘ 𝐾 ) ∀ 𝑤 ∈ ( Base ‘ 𝐾 ) ( ( ( 𝑟 ( ·𝑠𝐾 ) 𝑧 ) ( .r𝐾 ) 𝑤 ) = ( 𝑟 ( ·𝑠𝐾 ) ( 𝑧 ( .r𝐾 ) 𝑤 ) ) ∧ ( 𝑧 ( .r𝐾 ) ( 𝑟 ( ·𝑠𝐾 ) 𝑤 ) ) = ( 𝑟 ( ·𝑠𝐾 ) ( 𝑧 ( .r𝐾 ) 𝑤 ) ) ) ) )
76 72 75 raleqbidv ( ( 𝜑 ∧ ( 𝐾 ∈ LMod ∧ 𝐾 ∈ Ring ) ) → ( ∀ 𝑟𝑃𝑧𝐵𝑤𝐵 ( ( ( 𝑟 ( ·𝑠𝐾 ) 𝑧 ) ( .r𝐾 ) 𝑤 ) = ( 𝑟 ( ·𝑠𝐾 ) ( 𝑧 ( .r𝐾 ) 𝑤 ) ) ∧ ( 𝑧 ( .r𝐾 ) ( 𝑟 ( ·𝑠𝐾 ) 𝑤 ) ) = ( 𝑟 ( ·𝑠𝐾 ) ( 𝑧 ( .r𝐾 ) 𝑤 ) ) ) ↔ ∀ 𝑟 ∈ ( Base ‘ ( Scalar ‘ 𝐾 ) ) ∀ 𝑧 ∈ ( Base ‘ 𝐾 ) ∀ 𝑤 ∈ ( Base ‘ 𝐾 ) ( ( ( 𝑟 ( ·𝑠𝐾 ) 𝑧 ) ( .r𝐾 ) 𝑤 ) = ( 𝑟 ( ·𝑠𝐾 ) ( 𝑧 ( .r𝐾 ) 𝑤 ) ) ∧ ( 𝑧 ( .r𝐾 ) ( 𝑟 ( ·𝑠𝐾 ) 𝑤 ) ) = ( 𝑟 ( ·𝑠𝐾 ) ( 𝑧 ( .r𝐾 ) 𝑤 ) ) ) ) )
77 6 fveq2d ( 𝜑 → ( Base ‘ 𝐹 ) = ( Base ‘ ( Scalar ‘ 𝐿 ) ) )
78 7 77 eqtrid ( 𝜑𝑃 = ( Base ‘ ( Scalar ‘ 𝐿 ) ) )
79 78 adantr ( ( 𝜑 ∧ ( 𝐾 ∈ LMod ∧ 𝐾 ∈ Ring ) ) → 𝑃 = ( Base ‘ ( Scalar ‘ 𝐿 ) ) )
80 2 adantr ( ( 𝜑 ∧ ( 𝐾 ∈ LMod ∧ 𝐾 ∈ Ring ) ) → 𝐵 = ( Base ‘ 𝐿 ) )
81 80 raleqdv ( ( 𝜑 ∧ ( 𝐾 ∈ LMod ∧ 𝐾 ∈ Ring ) ) → ( ∀ 𝑤𝐵 ( ( ( 𝑟 ( ·𝑠𝐿 ) 𝑧 ) ( .r𝐿 ) 𝑤 ) = ( 𝑟 ( ·𝑠𝐿 ) ( 𝑧 ( .r𝐿 ) 𝑤 ) ) ∧ ( 𝑧 ( .r𝐿 ) ( 𝑟 ( ·𝑠𝐿 ) 𝑤 ) ) = ( 𝑟 ( ·𝑠𝐿 ) ( 𝑧 ( .r𝐿 ) 𝑤 ) ) ) ↔ ∀ 𝑤 ∈ ( Base ‘ 𝐿 ) ( ( ( 𝑟 ( ·𝑠𝐿 ) 𝑧 ) ( .r𝐿 ) 𝑤 ) = ( 𝑟 ( ·𝑠𝐿 ) ( 𝑧 ( .r𝐿 ) 𝑤 ) ) ∧ ( 𝑧 ( .r𝐿 ) ( 𝑟 ( ·𝑠𝐿 ) 𝑤 ) ) = ( 𝑟 ( ·𝑠𝐿 ) ( 𝑧 ( .r𝐿 ) 𝑤 ) ) ) ) )
82 80 81 raleqbidv ( ( 𝜑 ∧ ( 𝐾 ∈ LMod ∧ 𝐾 ∈ Ring ) ) → ( ∀ 𝑧𝐵𝑤𝐵 ( ( ( 𝑟 ( ·𝑠𝐿 ) 𝑧 ) ( .r𝐿 ) 𝑤 ) = ( 𝑟 ( ·𝑠𝐿 ) ( 𝑧 ( .r𝐿 ) 𝑤 ) ) ∧ ( 𝑧 ( .r𝐿 ) ( 𝑟 ( ·𝑠𝐿 ) 𝑤 ) ) = ( 𝑟 ( ·𝑠𝐿 ) ( 𝑧 ( .r𝐿 ) 𝑤 ) ) ) ↔ ∀ 𝑧 ∈ ( Base ‘ 𝐿 ) ∀ 𝑤 ∈ ( Base ‘ 𝐿 ) ( ( ( 𝑟 ( ·𝑠𝐿 ) 𝑧 ) ( .r𝐿 ) 𝑤 ) = ( 𝑟 ( ·𝑠𝐿 ) ( 𝑧 ( .r𝐿 ) 𝑤 ) ) ∧ ( 𝑧 ( .r𝐿 ) ( 𝑟 ( ·𝑠𝐿 ) 𝑤 ) ) = ( 𝑟 ( ·𝑠𝐿 ) ( 𝑧 ( .r𝐿 ) 𝑤 ) ) ) ) )
83 79 82 raleqbidv ( ( 𝜑 ∧ ( 𝐾 ∈ LMod ∧ 𝐾 ∈ Ring ) ) → ( ∀ 𝑟𝑃𝑧𝐵𝑤𝐵 ( ( ( 𝑟 ( ·𝑠𝐿 ) 𝑧 ) ( .r𝐿 ) 𝑤 ) = ( 𝑟 ( ·𝑠𝐿 ) ( 𝑧 ( .r𝐿 ) 𝑤 ) ) ∧ ( 𝑧 ( .r𝐿 ) ( 𝑟 ( ·𝑠𝐿 ) 𝑤 ) ) = ( 𝑟 ( ·𝑠𝐿 ) ( 𝑧 ( .r𝐿 ) 𝑤 ) ) ) ↔ ∀ 𝑟 ∈ ( Base ‘ ( Scalar ‘ 𝐿 ) ) ∀ 𝑧 ∈ ( Base ‘ 𝐿 ) ∀ 𝑤 ∈ ( Base ‘ 𝐿 ) ( ( ( 𝑟 ( ·𝑠𝐿 ) 𝑧 ) ( .r𝐿 ) 𝑤 ) = ( 𝑟 ( ·𝑠𝐿 ) ( 𝑧 ( .r𝐿 ) 𝑤 ) ) ∧ ( 𝑧 ( .r𝐿 ) ( 𝑟 ( ·𝑠𝐿 ) 𝑤 ) ) = ( 𝑟 ( ·𝑠𝐿 ) ( 𝑧 ( .r𝐿 ) 𝑤 ) ) ) ) )
84 71 76 83 3bitr3d ( ( 𝜑 ∧ ( 𝐾 ∈ LMod ∧ 𝐾 ∈ Ring ) ) → ( ∀ 𝑟 ∈ ( Base ‘ ( Scalar ‘ 𝐾 ) ) ∀ 𝑧 ∈ ( Base ‘ 𝐾 ) ∀ 𝑤 ∈ ( Base ‘ 𝐾 ) ( ( ( 𝑟 ( ·𝑠𝐾 ) 𝑧 ) ( .r𝐾 ) 𝑤 ) = ( 𝑟 ( ·𝑠𝐾 ) ( 𝑧 ( .r𝐾 ) 𝑤 ) ) ∧ ( 𝑧 ( .r𝐾 ) ( 𝑟 ( ·𝑠𝐾 ) 𝑤 ) ) = ( 𝑟 ( ·𝑠𝐾 ) ( 𝑧 ( .r𝐾 ) 𝑤 ) ) ) ↔ ∀ 𝑟 ∈ ( Base ‘ ( Scalar ‘ 𝐿 ) ) ∀ 𝑧 ∈ ( Base ‘ 𝐿 ) ∀ 𝑤 ∈ ( Base ‘ 𝐿 ) ( ( ( 𝑟 ( ·𝑠𝐿 ) 𝑧 ) ( .r𝐿 ) 𝑤 ) = ( 𝑟 ( ·𝑠𝐿 ) ( 𝑧 ( .r𝐿 ) 𝑤 ) ) ∧ ( 𝑧 ( .r𝐿 ) ( 𝑟 ( ·𝑠𝐿 ) 𝑤 ) ) = ( 𝑟 ( ·𝑠𝐿 ) ( 𝑧 ( .r𝐿 ) 𝑤 ) ) ) ) )
85 21 84 anbi12d ( ( 𝜑 ∧ ( 𝐾 ∈ LMod ∧ 𝐾 ∈ Ring ) ) → ( ( ( 𝐾 ∈ LMod ∧ 𝐾 ∈ Ring ) ∧ ∀ 𝑟 ∈ ( Base ‘ ( Scalar ‘ 𝐾 ) ) ∀ 𝑧 ∈ ( Base ‘ 𝐾 ) ∀ 𝑤 ∈ ( Base ‘ 𝐾 ) ( ( ( 𝑟 ( ·𝑠𝐾 ) 𝑧 ) ( .r𝐾 ) 𝑤 ) = ( 𝑟 ( ·𝑠𝐾 ) ( 𝑧 ( .r𝐾 ) 𝑤 ) ) ∧ ( 𝑧 ( .r𝐾 ) ( 𝑟 ( ·𝑠𝐾 ) 𝑤 ) ) = ( 𝑟 ( ·𝑠𝐾 ) ( 𝑧 ( .r𝐾 ) 𝑤 ) ) ) ) ↔ ( ( 𝐿 ∈ LMod ∧ 𝐿 ∈ Ring ) ∧ ∀ 𝑟 ∈ ( Base ‘ ( Scalar ‘ 𝐿 ) ) ∀ 𝑧 ∈ ( Base ‘ 𝐿 ) ∀ 𝑤 ∈ ( Base ‘ 𝐿 ) ( ( ( 𝑟 ( ·𝑠𝐿 ) 𝑧 ) ( .r𝐿 ) 𝑤 ) = ( 𝑟 ( ·𝑠𝐿 ) ( 𝑧 ( .r𝐿 ) 𝑤 ) ) ∧ ( 𝑧 ( .r𝐿 ) ( 𝑟 ( ·𝑠𝐿 ) 𝑤 ) ) = ( 𝑟 ( ·𝑠𝐿 ) ( 𝑧 ( .r𝐿 ) 𝑤 ) ) ) ) ) )
86 32 33 35 34 46 isassa ( 𝐾 ∈ AssAlg ↔ ( ( 𝐾 ∈ LMod ∧ 𝐾 ∈ Ring ) ∧ ∀ 𝑟 ∈ ( Base ‘ ( Scalar ‘ 𝐾 ) ) ∀ 𝑧 ∈ ( Base ‘ 𝐾 ) ∀ 𝑤 ∈ ( Base ‘ 𝐾 ) ( ( ( 𝑟 ( ·𝑠𝐾 ) 𝑧 ) ( .r𝐾 ) 𝑤 ) = ( 𝑟 ( ·𝑠𝐾 ) ( 𝑧 ( .r𝐾 ) 𝑤 ) ) ∧ ( 𝑧 ( .r𝐾 ) ( 𝑟 ( ·𝑠𝐾 ) 𝑤 ) ) = ( 𝑟 ( ·𝑠𝐾 ) ( 𝑧 ( .r𝐾 ) 𝑤 ) ) ) ) )
87 eqid ( Base ‘ 𝐿 ) = ( Base ‘ 𝐿 )
88 eqid ( Scalar ‘ 𝐿 ) = ( Scalar ‘ 𝐿 )
89 eqid ( Base ‘ ( Scalar ‘ 𝐿 ) ) = ( Base ‘ ( Scalar ‘ 𝐿 ) )
90 eqid ( ·𝑠𝐿 ) = ( ·𝑠𝐿 )
91 eqid ( .r𝐿 ) = ( .r𝐿 )
92 87 88 89 90 91 isassa ( 𝐿 ∈ AssAlg ↔ ( ( 𝐿 ∈ LMod ∧ 𝐿 ∈ Ring ) ∧ ∀ 𝑟 ∈ ( Base ‘ ( Scalar ‘ 𝐿 ) ) ∀ 𝑧 ∈ ( Base ‘ 𝐿 ) ∀ 𝑤 ∈ ( Base ‘ 𝐿 ) ( ( ( 𝑟 ( ·𝑠𝐿 ) 𝑧 ) ( .r𝐿 ) 𝑤 ) = ( 𝑟 ( ·𝑠𝐿 ) ( 𝑧 ( .r𝐿 ) 𝑤 ) ) ∧ ( 𝑧 ( .r𝐿 ) ( 𝑟 ( ·𝑠𝐿 ) 𝑤 ) ) = ( 𝑟 ( ·𝑠𝐿 ) ( 𝑧 ( .r𝐿 ) 𝑤 ) ) ) ) )
93 85 86 92 3bitr4g ( ( 𝜑 ∧ ( 𝐾 ∈ LMod ∧ 𝐾 ∈ Ring ) ) → ( 𝐾 ∈ AssAlg ↔ 𝐿 ∈ AssAlg ) )
94 93 ex ( 𝜑 → ( ( 𝐾 ∈ LMod ∧ 𝐾 ∈ Ring ) → ( 𝐾 ∈ AssAlg ↔ 𝐿 ∈ AssAlg ) ) )
95 12 19 94 pm5.21ndd ( 𝜑 → ( 𝐾 ∈ AssAlg ↔ 𝐿 ∈ AssAlg ) )