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