This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem sraassab

Description: A subring algebra is an associative algebra if and only if the subring is included in the ring's center. (Contributed by SN, 21-Mar-2025)

Ref Expression
Hypotheses sraassab.a ⊢ 𝐴 = ( ( subringAlg ‘ 𝑊 ) ‘ 𝑆 )
sraassab.z ⊢ 𝑍 = ( Cntr ‘ ( mulGrp ‘ 𝑊 ) )
sraassab.w ⊢ ( 𝜑 → 𝑊 ∈ Ring )
sraassab.s ⊢ ( 𝜑 → 𝑆 ∈ ( SubRing ‘ 𝑊 ) )
Assertion sraassab ( 𝜑 → ( 𝐴 ∈ AssAlg ↔ 𝑆 ⊆ 𝑍 ) )

Proof

Step Hyp Ref Expression
1 sraassab.a ⊢ 𝐴 = ( ( subringAlg ‘ 𝑊 ) ‘ 𝑆 )
2 sraassab.z ⊢ 𝑍 = ( Cntr ‘ ( mulGrp ‘ 𝑊 ) )
3 sraassab.w ⊢ ( 𝜑 → 𝑊 ∈ Ring )
4 sraassab.s ⊢ ( 𝜑 → 𝑆 ∈ ( SubRing ‘ 𝑊 ) )
5 eqid ⊢ ( Base ‘ 𝑊 ) = ( Base ‘ 𝑊 )
6 5 subrgss ⊢ ( 𝑆 ∈ ( SubRing ‘ 𝑊 ) → 𝑆 ⊆ ( Base ‘ 𝑊 ) )
7 4 6 syl ⊢ ( 𝜑 → 𝑆 ⊆ ( Base ‘ 𝑊 ) )
8 7 adantr ⊢ ( ( 𝜑 ∧ 𝐴 ∈ AssAlg ) → 𝑆 ⊆ ( Base ‘ 𝑊 ) )
9 8 sselda ⊢ ( ( ( 𝜑 ∧ 𝐴 ∈ AssAlg ) ∧ 𝑦 ∈ 𝑆 ) → 𝑦 ∈ ( Base ‘ 𝑊 ) )
10 simpllr ⊢ ( ( ( ( 𝜑 ∧ 𝐴 ∈ AssAlg ) ∧ 𝑦 ∈ 𝑆 ) ∧ 𝑥 ∈ ( Base ‘ 𝑊 ) ) → 𝐴 ∈ AssAlg )
11 eqid ⊢ ( 𝑊 ↾s 𝑆 ) = ( 𝑊 ↾s 𝑆 )
12 11 subrgbas ⊢ ( 𝑆 ∈ ( SubRing ‘ 𝑊 ) → 𝑆 = ( Base ‘ ( 𝑊 ↾s 𝑆 ) ) )
13 4 12 syl ⊢ ( 𝜑 → 𝑆 = ( Base ‘ ( 𝑊 ↾s 𝑆 ) ) )
14 1 a1i ⊢ ( 𝜑 → 𝐴 = ( ( subringAlg ‘ 𝑊 ) ‘ 𝑆 ) )
15 14 7 srasca ⊢ ( 𝜑 → ( 𝑊 ↾s 𝑆 ) = ( Scalar ‘ 𝐴 ) )
16 15 fveq2d ⊢ ( 𝜑 → ( Base ‘ ( 𝑊 ↾s 𝑆 ) ) = ( Base ‘ ( Scalar ‘ 𝐴 ) ) )
17 13 16 eqtrd ⊢ ( 𝜑 → 𝑆 = ( Base ‘ ( Scalar ‘ 𝐴 ) ) )
18 17 eqimssd ⊢ ( 𝜑 → 𝑆 ⊆ ( Base ‘ ( Scalar ‘ 𝐴 ) ) )
19 18 sselda ⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝑆 ) → 𝑦 ∈ ( Base ‘ ( Scalar ‘ 𝐴 ) ) )
20 19 ad4ant13 ⊢ ( ( ( ( 𝜑 ∧ 𝐴 ∈ AssAlg ) ∧ 𝑦 ∈ 𝑆 ) ∧ 𝑥 ∈ ( Base ‘ 𝑊 ) ) → 𝑦 ∈ ( Base ‘ ( Scalar ‘ 𝐴 ) ) )
21 14 7 srabase ⊢ ( 𝜑 → ( Base ‘ 𝑊 ) = ( Base ‘ 𝐴 ) )
22 21 eqimssd ⊢ ( 𝜑 → ( Base ‘ 𝑊 ) ⊆ ( Base ‘ 𝐴 ) )
23 22 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝐴 ∈ AssAlg ) ∧ 𝑦 ∈ 𝑆 ) → ( Base ‘ 𝑊 ) ⊆ ( Base ‘ 𝐴 ) )
24 23 sselda ⊢ ( ( ( ( 𝜑 ∧ 𝐴 ∈ AssAlg ) ∧ 𝑦 ∈ 𝑆 ) ∧ 𝑥 ∈ ( Base ‘ 𝑊 ) ) → 𝑥 ∈ ( Base ‘ 𝐴 ) )
25 eqid ⊢ ( 1r ‘ 𝑊 ) = ( 1r ‘ 𝑊 )
26 5 25 ringidcl ⊢ ( 𝑊 ∈ Ring → ( 1r ‘ 𝑊 ) ∈ ( Base ‘ 𝑊 ) )
27 3 26 syl ⊢ ( 𝜑 → ( 1r ‘ 𝑊 ) ∈ ( Base ‘ 𝑊 ) )
28 27 21 eleqtrd ⊢ ( 𝜑 → ( 1r ‘ 𝑊 ) ∈ ( Base ‘ 𝐴 ) )
29 28 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ 𝐴 ∈ AssAlg ) ∧ 𝑦 ∈ 𝑆 ) ∧ 𝑥 ∈ ( Base ‘ 𝑊 ) ) → ( 1r ‘ 𝑊 ) ∈ ( Base ‘ 𝐴 ) )
30 eqid ⊢ ( Base ‘ 𝐴 ) = ( Base ‘ 𝐴 )
31 eqid ⊢ ( Scalar ‘ 𝐴 ) = ( Scalar ‘ 𝐴 )
32 eqid ⊢ ( Base ‘ ( Scalar ‘ 𝐴 ) ) = ( Base ‘ ( Scalar ‘ 𝐴 ) )
33 eqid ⊢ ( ·𝑠 ‘ 𝐴 ) = ( ·𝑠 ‘ 𝐴 )
34 eqid ⊢ ( .r ‘ 𝐴 ) = ( .r ‘ 𝐴 )
35 30 31 32 33 34 assaassr ⊢ ( ( 𝐴 ∈ AssAlg ∧ ( 𝑦 ∈ ( Base ‘ ( Scalar ‘ 𝐴 ) ) ∧ 𝑥 ∈ ( Base ‘ 𝐴 ) ∧ ( 1r ‘ 𝑊 ) ∈ ( Base ‘ 𝐴 ) ) ) → ( 𝑥 ( .r ‘ 𝐴 ) ( 𝑦 ( ·𝑠 ‘ 𝐴 ) ( 1r ‘ 𝑊 ) ) ) = ( 𝑦 ( ·𝑠 ‘ 𝐴 ) ( 𝑥 ( .r ‘ 𝐴 ) ( 1r ‘ 𝑊 ) ) ) )
36 10 20 24 29 35 syl13anc ⊢ ( ( ( ( 𝜑 ∧ 𝐴 ∈ AssAlg ) ∧ 𝑦 ∈ 𝑆 ) ∧ 𝑥 ∈ ( Base ‘ 𝑊 ) ) → ( 𝑥 ( .r ‘ 𝐴 ) ( 𝑦 ( ·𝑠 ‘ 𝐴 ) ( 1r ‘ 𝑊 ) ) ) = ( 𝑦 ( ·𝑠 ‘ 𝐴 ) ( 𝑥 ( .r ‘ 𝐴 ) ( 1r ‘ 𝑊 ) ) ) )
37 14 7 sramulr ⊢ ( 𝜑 → ( .r ‘ 𝑊 ) = ( .r ‘ 𝐴 ) )
38 37 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ 𝐴 ∈ AssAlg ) ∧ 𝑦 ∈ 𝑆 ) ∧ 𝑥 ∈ ( Base ‘ 𝑊 ) ) → ( .r ‘ 𝑊 ) = ( .r ‘ 𝐴 ) )
39 38 oveqd ⊢ ( ( ( ( 𝜑 ∧ 𝐴 ∈ AssAlg ) ∧ 𝑦 ∈ 𝑆 ) ∧ 𝑥 ∈ ( Base ‘ 𝑊 ) ) → ( 𝑥 ( .r ‘ 𝑊 ) ( 𝑦 ( ·𝑠 ‘ 𝐴 ) ( 1r ‘ 𝑊 ) ) ) = ( 𝑥 ( .r ‘ 𝐴 ) ( 𝑦 ( ·𝑠 ‘ 𝐴 ) ( 1r ‘ 𝑊 ) ) ) )
40 14 7 sravsca ⊢ ( 𝜑 → ( .r ‘ 𝑊 ) = ( ·𝑠 ‘ 𝐴 ) )
41 40 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ 𝐴 ∈ AssAlg ) ∧ 𝑦 ∈ 𝑆 ) ∧ 𝑥 ∈ ( Base ‘ 𝑊 ) ) → ( .r ‘ 𝑊 ) = ( ·𝑠 ‘ 𝐴 ) )
42 41 oveqd ⊢ ( ( ( ( 𝜑 ∧ 𝐴 ∈ AssAlg ) ∧ 𝑦 ∈ 𝑆 ) ∧ 𝑥 ∈ ( Base ‘ 𝑊 ) ) → ( 𝑦 ( .r ‘ 𝑊 ) ( 1r ‘ 𝑊 ) ) = ( 𝑦 ( ·𝑠 ‘ 𝐴 ) ( 1r ‘ 𝑊 ) ) )
43 eqid ⊢ ( .r ‘ 𝑊 ) = ( .r ‘ 𝑊 )
44 3 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ 𝐴 ∈ AssAlg ) ∧ 𝑦 ∈ 𝑆 ) ∧ 𝑥 ∈ ( Base ‘ 𝑊 ) ) → 𝑊 ∈ Ring )
45 9 adantr ⊢ ( ( ( ( 𝜑 ∧ 𝐴 ∈ AssAlg ) ∧ 𝑦 ∈ 𝑆 ) ∧ 𝑥 ∈ ( Base ‘ 𝑊 ) ) → 𝑦 ∈ ( Base ‘ 𝑊 ) )
46 5 43 25 44 45 ringridmd ⊢ ( ( ( ( 𝜑 ∧ 𝐴 ∈ AssAlg ) ∧ 𝑦 ∈ 𝑆 ) ∧ 𝑥 ∈ ( Base ‘ 𝑊 ) ) → ( 𝑦 ( .r ‘ 𝑊 ) ( 1r ‘ 𝑊 ) ) = 𝑦 )
47 42 46 eqtr3d ⊢ ( ( ( ( 𝜑 ∧ 𝐴 ∈ AssAlg ) ∧ 𝑦 ∈ 𝑆 ) ∧ 𝑥 ∈ ( Base ‘ 𝑊 ) ) → ( 𝑦 ( ·𝑠 ‘ 𝐴 ) ( 1r ‘ 𝑊 ) ) = 𝑦 )
48 47 oveq2d ⊢ ( ( ( ( 𝜑 ∧ 𝐴 ∈ AssAlg ) ∧ 𝑦 ∈ 𝑆 ) ∧ 𝑥 ∈ ( Base ‘ 𝑊 ) ) → ( 𝑥 ( .r ‘ 𝑊 ) ( 𝑦 ( ·𝑠 ‘ 𝐴 ) ( 1r ‘ 𝑊 ) ) ) = ( 𝑥 ( .r ‘ 𝑊 ) 𝑦 ) )
49 39 48 eqtr3d ⊢ ( ( ( ( 𝜑 ∧ 𝐴 ∈ AssAlg ) ∧ 𝑦 ∈ 𝑆 ) ∧ 𝑥 ∈ ( Base ‘ 𝑊 ) ) → ( 𝑥 ( .r ‘ 𝐴 ) ( 𝑦 ( ·𝑠 ‘ 𝐴 ) ( 1r ‘ 𝑊 ) ) ) = ( 𝑥 ( .r ‘ 𝑊 ) 𝑦 ) )
50 41 oveqd ⊢ ( ( ( ( 𝜑 ∧ 𝐴 ∈ AssAlg ) ∧ 𝑦 ∈ 𝑆 ) ∧ 𝑥 ∈ ( Base ‘ 𝑊 ) ) → ( 𝑦 ( .r ‘ 𝑊 ) ( 𝑥 ( .r ‘ 𝐴 ) ( 1r ‘ 𝑊 ) ) ) = ( 𝑦 ( ·𝑠 ‘ 𝐴 ) ( 𝑥 ( .r ‘ 𝐴 ) ( 1r ‘ 𝑊 ) ) ) )
51 38 oveqd ⊢ ( ( ( ( 𝜑 ∧ 𝐴 ∈ AssAlg ) ∧ 𝑦 ∈ 𝑆 ) ∧ 𝑥 ∈ ( Base ‘ 𝑊 ) ) → ( 𝑥 ( .r ‘ 𝑊 ) ( 1r ‘ 𝑊 ) ) = ( 𝑥 ( .r ‘ 𝐴 ) ( 1r ‘ 𝑊 ) ) )
52 simpr ⊢ ( ( ( ( 𝜑 ∧ 𝐴 ∈ AssAlg ) ∧ 𝑦 ∈ 𝑆 ) ∧ 𝑥 ∈ ( Base ‘ 𝑊 ) ) → 𝑥 ∈ ( Base ‘ 𝑊 ) )
53 5 43 25 44 52 ringridmd ⊢ ( ( ( ( 𝜑 ∧ 𝐴 ∈ AssAlg ) ∧ 𝑦 ∈ 𝑆 ) ∧ 𝑥 ∈ ( Base ‘ 𝑊 ) ) → ( 𝑥 ( .r ‘ 𝑊 ) ( 1r ‘ 𝑊 ) ) = 𝑥 )
54 51 53 eqtr3d ⊢ ( ( ( ( 𝜑 ∧ 𝐴 ∈ AssAlg ) ∧ 𝑦 ∈ 𝑆 ) ∧ 𝑥 ∈ ( Base ‘ 𝑊 ) ) → ( 𝑥 ( .r ‘ 𝐴 ) ( 1r ‘ 𝑊 ) ) = 𝑥 )
55 54 oveq2d ⊢ ( ( ( ( 𝜑 ∧ 𝐴 ∈ AssAlg ) ∧ 𝑦 ∈ 𝑆 ) ∧ 𝑥 ∈ ( Base ‘ 𝑊 ) ) → ( 𝑦 ( .r ‘ 𝑊 ) ( 𝑥 ( .r ‘ 𝐴 ) ( 1r ‘ 𝑊 ) ) ) = ( 𝑦 ( .r ‘ 𝑊 ) 𝑥 ) )
56 50 55 eqtr3d ⊢ ( ( ( ( 𝜑 ∧ 𝐴 ∈ AssAlg ) ∧ 𝑦 ∈ 𝑆 ) ∧ 𝑥 ∈ ( Base ‘ 𝑊 ) ) → ( 𝑦 ( ·𝑠 ‘ 𝐴 ) ( 𝑥 ( .r ‘ 𝐴 ) ( 1r ‘ 𝑊 ) ) ) = ( 𝑦 ( .r ‘ 𝑊 ) 𝑥 ) )
57 36 49 56 3eqtr3rd ⊢ ( ( ( ( 𝜑 ∧ 𝐴 ∈ AssAlg ) ∧ 𝑦 ∈ 𝑆 ) ∧ 𝑥 ∈ ( Base ‘ 𝑊 ) ) → ( 𝑦 ( .r ‘ 𝑊 ) 𝑥 ) = ( 𝑥 ( .r ‘ 𝑊 ) 𝑦 ) )
58 57 ralrimiva ⊢ ( ( ( 𝜑 ∧ 𝐴 ∈ AssAlg ) ∧ 𝑦 ∈ 𝑆 ) → ∀ 𝑥 ∈ ( Base ‘ 𝑊 ) ( 𝑦 ( .r ‘ 𝑊 ) 𝑥 ) = ( 𝑥 ( .r ‘ 𝑊 ) 𝑦 ) )
59 eqid ⊢ ( mulGrp ‘ 𝑊 ) = ( mulGrp ‘ 𝑊 )
60 59 5 mgpbas ⊢ ( Base ‘ 𝑊 ) = ( Base ‘ ( mulGrp ‘ 𝑊 ) )
61 59 43 mgpplusg ⊢ ( .r ‘ 𝑊 ) = ( +g ‘ ( mulGrp ‘ 𝑊 ) )
62 60 61 2 elcntr ⊢ ( 𝑦 ∈ 𝑍 ↔ ( 𝑦 ∈ ( Base ‘ 𝑊 ) ∧ ∀ 𝑥 ∈ ( Base ‘ 𝑊 ) ( 𝑦 ( .r ‘ 𝑊 ) 𝑥 ) = ( 𝑥 ( .r ‘ 𝑊 ) 𝑦 ) ) )
63 9 58 62 sylanbrc ⊢ ( ( ( 𝜑 ∧ 𝐴 ∈ AssAlg ) ∧ 𝑦 ∈ 𝑆 ) → 𝑦 ∈ 𝑍 )
64 63 ex ⊢ ( ( 𝜑 ∧ 𝐴 ∈ AssAlg ) → ( 𝑦 ∈ 𝑆 → 𝑦 ∈ 𝑍 ) )
65 64 ssrdv ⊢ ( ( 𝜑 ∧ 𝐴 ∈ AssAlg ) → 𝑆 ⊆ 𝑍 )
66 21 adantr ⊢ ( ( 𝜑 ∧ 𝑆 ⊆ 𝑍 ) → ( Base ‘ 𝑊 ) = ( Base ‘ 𝐴 ) )
67 15 adantr ⊢ ( ( 𝜑 ∧ 𝑆 ⊆ 𝑍 ) → ( 𝑊 ↾s 𝑆 ) = ( Scalar ‘ 𝐴 ) )
68 13 adantr ⊢ ( ( 𝜑 ∧ 𝑆 ⊆ 𝑍 ) → 𝑆 = ( Base ‘ ( 𝑊 ↾s 𝑆 ) ) )
69 40 adantr ⊢ ( ( 𝜑 ∧ 𝑆 ⊆ 𝑍 ) → ( .r ‘ 𝑊 ) = ( ·𝑠 ‘ 𝐴 ) )
70 37 adantr ⊢ ( ( 𝜑 ∧ 𝑆 ⊆ 𝑍 ) → ( .r ‘ 𝑊 ) = ( .r ‘ 𝐴 ) )
71 1 sralmod ⊢ ( 𝑆 ∈ ( SubRing ‘ 𝑊 ) → 𝐴 ∈ LMod )
72 4 71 syl ⊢ ( 𝜑 → 𝐴 ∈ LMod )
73 72 adantr ⊢ ( ( 𝜑 ∧ 𝑆 ⊆ 𝑍 ) → 𝐴 ∈ LMod )
74 1 5 sraring ⊢ ( ( 𝑊 ∈ Ring ∧ 𝑆 ⊆ ( Base ‘ 𝑊 ) ) → 𝐴 ∈ Ring )
75 3 7 74 syl2anc ⊢ ( 𝜑 → 𝐴 ∈ Ring )
76 75 adantr ⊢ ( ( 𝜑 ∧ 𝑆 ⊆ 𝑍 ) → 𝐴 ∈ Ring )
77 3 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑆 ⊆ 𝑍 ) ∧ ( 𝑥 ∈ 𝑆 ∧ 𝑦 ∈ ( Base ‘ 𝑊 ) ∧ 𝑧 ∈ ( Base ‘ 𝑊 ) ) ) → 𝑊 ∈ Ring )
78 7 adantr ⊢ ( ( 𝜑 ∧ 𝑆 ⊆ 𝑍 ) → 𝑆 ⊆ ( Base ‘ 𝑊 ) )
79 78 sselda ⊢ ( ( ( 𝜑 ∧ 𝑆 ⊆ 𝑍 ) ∧ 𝑥 ∈ 𝑆 ) → 𝑥 ∈ ( Base ‘ 𝑊 ) )
80 79 3ad2antr1 ⊢ ( ( ( 𝜑 ∧ 𝑆 ⊆ 𝑍 ) ∧ ( 𝑥 ∈ 𝑆 ∧ 𝑦 ∈ ( Base ‘ 𝑊 ) ∧ 𝑧 ∈ ( Base ‘ 𝑊 ) ) ) → 𝑥 ∈ ( Base ‘ 𝑊 ) )
81 simpr2 ⊢ ( ( ( 𝜑 ∧ 𝑆 ⊆ 𝑍 ) ∧ ( 𝑥 ∈ 𝑆 ∧ 𝑦 ∈ ( Base ‘ 𝑊 ) ∧ 𝑧 ∈ ( Base ‘ 𝑊 ) ) ) → 𝑦 ∈ ( Base ‘ 𝑊 ) )
82 simpr3 ⊢ ( ( ( 𝜑 ∧ 𝑆 ⊆ 𝑍 ) ∧ ( 𝑥 ∈ 𝑆 ∧ 𝑦 ∈ ( Base ‘ 𝑊 ) ∧ 𝑧 ∈ ( Base ‘ 𝑊 ) ) ) → 𝑧 ∈ ( Base ‘ 𝑊 ) )
83 5 43 77 80 81 82 ringassd ⊢ ( ( ( 𝜑 ∧ 𝑆 ⊆ 𝑍 ) ∧ ( 𝑥 ∈ 𝑆 ∧ 𝑦 ∈ ( Base ‘ 𝑊 ) ∧ 𝑧 ∈ ( Base ‘ 𝑊 ) ) ) → ( ( 𝑥 ( .r ‘ 𝑊 ) 𝑦 ) ( .r ‘ 𝑊 ) 𝑧 ) = ( 𝑥 ( .r ‘ 𝑊 ) ( 𝑦 ( .r ‘ 𝑊 ) 𝑧 ) ) )
84 ssel2 ⊢ ( ( 𝑆 ⊆ 𝑍 ∧ 𝑥 ∈ 𝑆 ) → 𝑥 ∈ 𝑍 )
85 84 ad2ant2lr ⊢ ( ( ( 𝜑 ∧ 𝑆 ⊆ 𝑍 ) ∧ ( 𝑥 ∈ 𝑆 ∧ 𝑦 ∈ ( Base ‘ 𝑊 ) ) ) → 𝑥 ∈ 𝑍 )
86 simprr ⊢ ( ( ( 𝜑 ∧ 𝑆 ⊆ 𝑍 ) ∧ ( 𝑥 ∈ 𝑆 ∧ 𝑦 ∈ ( Base ‘ 𝑊 ) ) ) → 𝑦 ∈ ( Base ‘ 𝑊 ) )
87 60 61 2 cntri ⊢ ( ( 𝑥 ∈ 𝑍 ∧ 𝑦 ∈ ( Base ‘ 𝑊 ) ) → ( 𝑥 ( .r ‘ 𝑊 ) 𝑦 ) = ( 𝑦 ( .r ‘ 𝑊 ) 𝑥 ) )
88 85 86 87 syl2anc ⊢ ( ( ( 𝜑 ∧ 𝑆 ⊆ 𝑍 ) ∧ ( 𝑥 ∈ 𝑆 ∧ 𝑦 ∈ ( Base ‘ 𝑊 ) ) ) → ( 𝑥 ( .r ‘ 𝑊 ) 𝑦 ) = ( 𝑦 ( .r ‘ 𝑊 ) 𝑥 ) )
89 88 3adantr3 ⊢ ( ( ( 𝜑 ∧ 𝑆 ⊆ 𝑍 ) ∧ ( 𝑥 ∈ 𝑆 ∧ 𝑦 ∈ ( Base ‘ 𝑊 ) ∧ 𝑧 ∈ ( Base ‘ 𝑊 ) ) ) → ( 𝑥 ( .r ‘ 𝑊 ) 𝑦 ) = ( 𝑦 ( .r ‘ 𝑊 ) 𝑥 ) )
90 89 oveq1d ⊢ ( ( ( 𝜑 ∧ 𝑆 ⊆ 𝑍 ) ∧ ( 𝑥 ∈ 𝑆 ∧ 𝑦 ∈ ( Base ‘ 𝑊 ) ∧ 𝑧 ∈ ( Base ‘ 𝑊 ) ) ) → ( ( 𝑥 ( .r ‘ 𝑊 ) 𝑦 ) ( .r ‘ 𝑊 ) 𝑧 ) = ( ( 𝑦 ( .r ‘ 𝑊 ) 𝑥 ) ( .r ‘ 𝑊 ) 𝑧 ) )
91 5 43 77 81 80 82 ringassd ⊢ ( ( ( 𝜑 ∧ 𝑆 ⊆ 𝑍 ) ∧ ( 𝑥 ∈ 𝑆 ∧ 𝑦 ∈ ( Base ‘ 𝑊 ) ∧ 𝑧 ∈ ( Base ‘ 𝑊 ) ) ) → ( ( 𝑦 ( .r ‘ 𝑊 ) 𝑥 ) ( .r ‘ 𝑊 ) 𝑧 ) = ( 𝑦 ( .r ‘ 𝑊 ) ( 𝑥 ( .r ‘ 𝑊 ) 𝑧 ) ) )
92 90 83 91 3eqtr3rd ⊢ ( ( ( 𝜑 ∧ 𝑆 ⊆ 𝑍 ) ∧ ( 𝑥 ∈ 𝑆 ∧ 𝑦 ∈ ( Base ‘ 𝑊 ) ∧ 𝑧 ∈ ( Base ‘ 𝑊 ) ) ) → ( 𝑦 ( .r ‘ 𝑊 ) ( 𝑥 ( .r ‘ 𝑊 ) 𝑧 ) ) = ( 𝑥 ( .r ‘ 𝑊 ) ( 𝑦 ( .r ‘ 𝑊 ) 𝑧 ) ) )
93 66 67 68 69 70 73 76 83 92 isassad ⊢ ( ( 𝜑 ∧ 𝑆 ⊆ 𝑍 ) → 𝐴 ∈ AssAlg )
94 65 93 impbida ⊢ ( 𝜑 → ( 𝐴 ∈ AssAlg ↔ 𝑆 ⊆ 𝑍 ) )