MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  isassa Structured version   Visualization version   GIF version

Theorem isassa 21278
Description: The properties of an associative algebra. (Contributed by Mario Carneiro, 29-Dec-2014.)
Hypotheses
Ref Expression
isassa.v 𝑉 = (Baseβ€˜π‘Š)
isassa.f 𝐹 = (Scalarβ€˜π‘Š)
isassa.b 𝐡 = (Baseβ€˜πΉ)
isassa.s Β· = ( ·𝑠 β€˜π‘Š)
isassa.t Γ— = (.rβ€˜π‘Š)
Assertion
Ref Expression
isassa (π‘Š ∈ AssAlg ↔ ((π‘Š ∈ LMod ∧ π‘Š ∈ Ring ∧ 𝐹 ∈ CRing) ∧ βˆ€π‘Ÿ ∈ 𝐡 βˆ€π‘₯ ∈ 𝑉 βˆ€π‘¦ ∈ 𝑉 (((π‘Ÿ Β· π‘₯) Γ— 𝑦) = (π‘Ÿ Β· (π‘₯ Γ— 𝑦)) ∧ (π‘₯ Γ— (π‘Ÿ Β· 𝑦)) = (π‘Ÿ Β· (π‘₯ Γ— 𝑦)))))
Distinct variable groups:   π‘₯,π‘Ÿ,𝑦   𝐡,π‘Ÿ   𝐹,π‘Ÿ   𝑉,π‘Ÿ,π‘₯,𝑦   Β· ,π‘Ÿ,π‘₯,𝑦   Γ— ,π‘Ÿ,π‘₯,𝑦   π‘Š,π‘Ÿ,π‘₯,𝑦
Allowed substitution hints:   𝐡(π‘₯,𝑦)   𝐹(π‘₯,𝑦)

Proof of Theorem isassa
Dummy variables 𝑓 𝑀 𝑠 𝑑 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 fvexd 6862 . . . 4 (𝑀 = π‘Š β†’ (Scalarβ€˜π‘€) ∈ V)
2 fveq2 6847 . . . . 5 (𝑀 = π‘Š β†’ (Scalarβ€˜π‘€) = (Scalarβ€˜π‘Š))
3 isassa.f . . . . 5 𝐹 = (Scalarβ€˜π‘Š)
42, 3eqtr4di 2795 . . . 4 (𝑀 = π‘Š β†’ (Scalarβ€˜π‘€) = 𝐹)
5 simpr 486 . . . . . 6 ((𝑀 = π‘Š ∧ 𝑓 = 𝐹) β†’ 𝑓 = 𝐹)
65eleq1d 2823 . . . . 5 ((𝑀 = π‘Š ∧ 𝑓 = 𝐹) β†’ (𝑓 ∈ CRing ↔ 𝐹 ∈ CRing))
75fveq2d 6851 . . . . . . 7 ((𝑀 = π‘Š ∧ 𝑓 = 𝐹) β†’ (Baseβ€˜π‘“) = (Baseβ€˜πΉ))
8 isassa.b . . . . . . 7 𝐡 = (Baseβ€˜πΉ)
97, 8eqtr4di 2795 . . . . . 6 ((𝑀 = π‘Š ∧ 𝑓 = 𝐹) β†’ (Baseβ€˜π‘“) = 𝐡)
10 fveq2 6847 . . . . . . . . 9 (𝑀 = π‘Š β†’ (Baseβ€˜π‘€) = (Baseβ€˜π‘Š))
11 isassa.v . . . . . . . . 9 𝑉 = (Baseβ€˜π‘Š)
1210, 11eqtr4di 2795 . . . . . . . 8 (𝑀 = π‘Š β†’ (Baseβ€˜π‘€) = 𝑉)
13 fvexd 6862 . . . . . . . . . 10 (𝑀 = π‘Š β†’ ( ·𝑠 β€˜π‘€) ∈ V)
14 fvexd 6862 . . . . . . . . . . 11 ((𝑀 = π‘Š ∧ 𝑠 = ( ·𝑠 β€˜π‘€)) β†’ (.rβ€˜π‘€) ∈ V)
15 simpr 486 . . . . . . . . . . . . . . 15 (((𝑀 = π‘Š ∧ 𝑠 = ( ·𝑠 β€˜π‘€)) ∧ 𝑑 = (.rβ€˜π‘€)) β†’ 𝑑 = (.rβ€˜π‘€))
16 fveq2 6847 . . . . . . . . . . . . . . . . 17 (𝑀 = π‘Š β†’ (.rβ€˜π‘€) = (.rβ€˜π‘Š))
1716ad2antrr 725 . . . . . . . . . . . . . . . 16 (((𝑀 = π‘Š ∧ 𝑠 = ( ·𝑠 β€˜π‘€)) ∧ 𝑑 = (.rβ€˜π‘€)) β†’ (.rβ€˜π‘€) = (.rβ€˜π‘Š))
18 isassa.t . . . . . . . . . . . . . . . 16 Γ— = (.rβ€˜π‘Š)
1917, 18eqtr4di 2795 . . . . . . . . . . . . . . 15 (((𝑀 = π‘Š ∧ 𝑠 = ( ·𝑠 β€˜π‘€)) ∧ 𝑑 = (.rβ€˜π‘€)) β†’ (.rβ€˜π‘€) = Γ— )
2015, 19eqtrd 2777 . . . . . . . . . . . . . 14 (((𝑀 = π‘Š ∧ 𝑠 = ( ·𝑠 β€˜π‘€)) ∧ 𝑑 = (.rβ€˜π‘€)) β†’ 𝑑 = Γ— )
21 simplr 768 . . . . . . . . . . . . . . . 16 (((𝑀 = π‘Š ∧ 𝑠 = ( ·𝑠 β€˜π‘€)) ∧ 𝑑 = (.rβ€˜π‘€)) β†’ 𝑠 = ( ·𝑠 β€˜π‘€))
22 fveq2 6847 . . . . . . . . . . . . . . . . . 18 (𝑀 = π‘Š β†’ ( ·𝑠 β€˜π‘€) = ( ·𝑠 β€˜π‘Š))
2322ad2antrr 725 . . . . . . . . . . . . . . . . 17 (((𝑀 = π‘Š ∧ 𝑠 = ( ·𝑠 β€˜π‘€)) ∧ 𝑑 = (.rβ€˜π‘€)) β†’ ( ·𝑠 β€˜π‘€) = ( ·𝑠 β€˜π‘Š))
24 isassa.s . . . . . . . . . . . . . . . . 17 Β· = ( ·𝑠 β€˜π‘Š)
2523, 24eqtr4di 2795 . . . . . . . . . . . . . . . 16 (((𝑀 = π‘Š ∧ 𝑠 = ( ·𝑠 β€˜π‘€)) ∧ 𝑑 = (.rβ€˜π‘€)) β†’ ( ·𝑠 β€˜π‘€) = Β· )
2621, 25eqtrd 2777 . . . . . . . . . . . . . . 15 (((𝑀 = π‘Š ∧ 𝑠 = ( ·𝑠 β€˜π‘€)) ∧ 𝑑 = (.rβ€˜π‘€)) β†’ 𝑠 = Β· )
2726oveqd 7379 . . . . . . . . . . . . . 14 (((𝑀 = π‘Š ∧ 𝑠 = ( ·𝑠 β€˜π‘€)) ∧ 𝑑 = (.rβ€˜π‘€)) β†’ (π‘Ÿπ‘ π‘₯) = (π‘Ÿ Β· π‘₯))
28 eqidd 2738 . . . . . . . . . . . . . 14 (((𝑀 = π‘Š ∧ 𝑠 = ( ·𝑠 β€˜π‘€)) ∧ 𝑑 = (.rβ€˜π‘€)) β†’ 𝑦 = 𝑦)
2920, 27, 28oveq123d 7383 . . . . . . . . . . . . 13 (((𝑀 = π‘Š ∧ 𝑠 = ( ·𝑠 β€˜π‘€)) ∧ 𝑑 = (.rβ€˜π‘€)) β†’ ((π‘Ÿπ‘ π‘₯)𝑑𝑦) = ((π‘Ÿ Β· π‘₯) Γ— 𝑦))
30 eqidd 2738 . . . . . . . . . . . . . 14 (((𝑀 = π‘Š ∧ 𝑠 = ( ·𝑠 β€˜π‘€)) ∧ 𝑑 = (.rβ€˜π‘€)) β†’ π‘Ÿ = π‘Ÿ)
3120oveqd 7379 . . . . . . . . . . . . . 14 (((𝑀 = π‘Š ∧ 𝑠 = ( ·𝑠 β€˜π‘€)) ∧ 𝑑 = (.rβ€˜π‘€)) β†’ (π‘₯𝑑𝑦) = (π‘₯ Γ— 𝑦))
3226, 30, 31oveq123d 7383 . . . . . . . . . . . . 13 (((𝑀 = π‘Š ∧ 𝑠 = ( ·𝑠 β€˜π‘€)) ∧ 𝑑 = (.rβ€˜π‘€)) β†’ (π‘Ÿπ‘ (π‘₯𝑑𝑦)) = (π‘Ÿ Β· (π‘₯ Γ— 𝑦)))
3329, 32eqeq12d 2753 . . . . . . . . . . . 12 (((𝑀 = π‘Š ∧ 𝑠 = ( ·𝑠 β€˜π‘€)) ∧ 𝑑 = (.rβ€˜π‘€)) β†’ (((π‘Ÿπ‘ π‘₯)𝑑𝑦) = (π‘Ÿπ‘ (π‘₯𝑑𝑦)) ↔ ((π‘Ÿ Β· π‘₯) Γ— 𝑦) = (π‘Ÿ Β· (π‘₯ Γ— 𝑦))))
34 eqidd 2738 . . . . . . . . . . . . . 14 (((𝑀 = π‘Š ∧ 𝑠 = ( ·𝑠 β€˜π‘€)) ∧ 𝑑 = (.rβ€˜π‘€)) β†’ π‘₯ = π‘₯)
3526oveqd 7379 . . . . . . . . . . . . . 14 (((𝑀 = π‘Š ∧ 𝑠 = ( ·𝑠 β€˜π‘€)) ∧ 𝑑 = (.rβ€˜π‘€)) β†’ (π‘Ÿπ‘ π‘¦) = (π‘Ÿ Β· 𝑦))
3620, 34, 35oveq123d 7383 . . . . . . . . . . . . 13 (((𝑀 = π‘Š ∧ 𝑠 = ( ·𝑠 β€˜π‘€)) ∧ 𝑑 = (.rβ€˜π‘€)) β†’ (π‘₯𝑑(π‘Ÿπ‘ π‘¦)) = (π‘₯ Γ— (π‘Ÿ Β· 𝑦)))
3736, 32eqeq12d 2753 . . . . . . . . . . . 12 (((𝑀 = π‘Š ∧ 𝑠 = ( ·𝑠 β€˜π‘€)) ∧ 𝑑 = (.rβ€˜π‘€)) β†’ ((π‘₯𝑑(π‘Ÿπ‘ π‘¦)) = (π‘Ÿπ‘ (π‘₯𝑑𝑦)) ↔ (π‘₯ Γ— (π‘Ÿ Β· 𝑦)) = (π‘Ÿ Β· (π‘₯ Γ— 𝑦))))
3833, 37anbi12d 632 . . . . . . . . . . 11 (((𝑀 = π‘Š ∧ 𝑠 = ( ·𝑠 β€˜π‘€)) ∧ 𝑑 = (.rβ€˜π‘€)) β†’ ((((π‘Ÿπ‘ π‘₯)𝑑𝑦) = (π‘Ÿπ‘ (π‘₯𝑑𝑦)) ∧ (π‘₯𝑑(π‘Ÿπ‘ π‘¦)) = (π‘Ÿπ‘ (π‘₯𝑑𝑦))) ↔ (((π‘Ÿ Β· π‘₯) Γ— 𝑦) = (π‘Ÿ Β· (π‘₯ Γ— 𝑦)) ∧ (π‘₯ Γ— (π‘Ÿ Β· 𝑦)) = (π‘Ÿ Β· (π‘₯ Γ— 𝑦)))))
3914, 38sbcied 3789 . . . . . . . . . 10 ((𝑀 = π‘Š ∧ 𝑠 = ( ·𝑠 β€˜π‘€)) β†’ ([(.rβ€˜π‘€) / 𝑑](((π‘Ÿπ‘ π‘₯)𝑑𝑦) = (π‘Ÿπ‘ (π‘₯𝑑𝑦)) ∧ (π‘₯𝑑(π‘Ÿπ‘ π‘¦)) = (π‘Ÿπ‘ (π‘₯𝑑𝑦))) ↔ (((π‘Ÿ Β· π‘₯) Γ— 𝑦) = (π‘Ÿ Β· (π‘₯ Γ— 𝑦)) ∧ (π‘₯ Γ— (π‘Ÿ Β· 𝑦)) = (π‘Ÿ Β· (π‘₯ Γ— 𝑦)))))
4013, 39sbcied 3789 . . . . . . . . 9 (𝑀 = π‘Š β†’ ([( ·𝑠 β€˜π‘€) / 𝑠][(.rβ€˜π‘€) / 𝑑](((π‘Ÿπ‘ π‘₯)𝑑𝑦) = (π‘Ÿπ‘ (π‘₯𝑑𝑦)) ∧ (π‘₯𝑑(π‘Ÿπ‘ π‘¦)) = (π‘Ÿπ‘ (π‘₯𝑑𝑦))) ↔ (((π‘Ÿ Β· π‘₯) Γ— 𝑦) = (π‘Ÿ Β· (π‘₯ Γ— 𝑦)) ∧ (π‘₯ Γ— (π‘Ÿ Β· 𝑦)) = (π‘Ÿ Β· (π‘₯ Γ— 𝑦)))))
4112, 40raleqbidv 3322 . . . . . . . 8 (𝑀 = π‘Š β†’ (βˆ€π‘¦ ∈ (Baseβ€˜π‘€)[( ·𝑠 β€˜π‘€) / 𝑠][(.rβ€˜π‘€) / 𝑑](((π‘Ÿπ‘ π‘₯)𝑑𝑦) = (π‘Ÿπ‘ (π‘₯𝑑𝑦)) ∧ (π‘₯𝑑(π‘Ÿπ‘ π‘¦)) = (π‘Ÿπ‘ (π‘₯𝑑𝑦))) ↔ βˆ€π‘¦ ∈ 𝑉 (((π‘Ÿ Β· π‘₯) Γ— 𝑦) = (π‘Ÿ Β· (π‘₯ Γ— 𝑦)) ∧ (π‘₯ Γ— (π‘Ÿ Β· 𝑦)) = (π‘Ÿ Β· (π‘₯ Γ— 𝑦)))))
4212, 41raleqbidv 3322 . . . . . . 7 (𝑀 = π‘Š β†’ (βˆ€π‘₯ ∈ (Baseβ€˜π‘€)βˆ€π‘¦ ∈ (Baseβ€˜π‘€)[( ·𝑠 β€˜π‘€) / 𝑠][(.rβ€˜π‘€) / 𝑑](((π‘Ÿπ‘ π‘₯)𝑑𝑦) = (π‘Ÿπ‘ (π‘₯𝑑𝑦)) ∧ (π‘₯𝑑(π‘Ÿπ‘ π‘¦)) = (π‘Ÿπ‘ (π‘₯𝑑𝑦))) ↔ βˆ€π‘₯ ∈ 𝑉 βˆ€π‘¦ ∈ 𝑉 (((π‘Ÿ Β· π‘₯) Γ— 𝑦) = (π‘Ÿ Β· (π‘₯ Γ— 𝑦)) ∧ (π‘₯ Γ— (π‘Ÿ Β· 𝑦)) = (π‘Ÿ Β· (π‘₯ Γ— 𝑦)))))
4342adantr 482 . . . . . 6 ((𝑀 = π‘Š ∧ 𝑓 = 𝐹) β†’ (βˆ€π‘₯ ∈ (Baseβ€˜π‘€)βˆ€π‘¦ ∈ (Baseβ€˜π‘€)[( ·𝑠 β€˜π‘€) / 𝑠][(.rβ€˜π‘€) / 𝑑](((π‘Ÿπ‘ π‘₯)𝑑𝑦) = (π‘Ÿπ‘ (π‘₯𝑑𝑦)) ∧ (π‘₯𝑑(π‘Ÿπ‘ π‘¦)) = (π‘Ÿπ‘ (π‘₯𝑑𝑦))) ↔ βˆ€π‘₯ ∈ 𝑉 βˆ€π‘¦ ∈ 𝑉 (((π‘Ÿ Β· π‘₯) Γ— 𝑦) = (π‘Ÿ Β· (π‘₯ Γ— 𝑦)) ∧ (π‘₯ Γ— (π‘Ÿ Β· 𝑦)) = (π‘Ÿ Β· (π‘₯ Γ— 𝑦)))))
449, 43raleqbidv 3322 . . . . 5 ((𝑀 = π‘Š ∧ 𝑓 = 𝐹) β†’ (βˆ€π‘Ÿ ∈ (Baseβ€˜π‘“)βˆ€π‘₯ ∈ (Baseβ€˜π‘€)βˆ€π‘¦ ∈ (Baseβ€˜π‘€)[( ·𝑠 β€˜π‘€) / 𝑠][(.rβ€˜π‘€) / 𝑑](((π‘Ÿπ‘ π‘₯)𝑑𝑦) = (π‘Ÿπ‘ (π‘₯𝑑𝑦)) ∧ (π‘₯𝑑(π‘Ÿπ‘ π‘¦)) = (π‘Ÿπ‘ (π‘₯𝑑𝑦))) ↔ βˆ€π‘Ÿ ∈ 𝐡 βˆ€π‘₯ ∈ 𝑉 βˆ€π‘¦ ∈ 𝑉 (((π‘Ÿ Β· π‘₯) Γ— 𝑦) = (π‘Ÿ Β· (π‘₯ Γ— 𝑦)) ∧ (π‘₯ Γ— (π‘Ÿ Β· 𝑦)) = (π‘Ÿ Β· (π‘₯ Γ— 𝑦)))))
456, 44anbi12d 632 . . . 4 ((𝑀 = π‘Š ∧ 𝑓 = 𝐹) β†’ ((𝑓 ∈ CRing ∧ βˆ€π‘Ÿ ∈ (Baseβ€˜π‘“)βˆ€π‘₯ ∈ (Baseβ€˜π‘€)βˆ€π‘¦ ∈ (Baseβ€˜π‘€)[( ·𝑠 β€˜π‘€) / 𝑠][(.rβ€˜π‘€) / 𝑑](((π‘Ÿπ‘ π‘₯)𝑑𝑦) = (π‘Ÿπ‘ (π‘₯𝑑𝑦)) ∧ (π‘₯𝑑(π‘Ÿπ‘ π‘¦)) = (π‘Ÿπ‘ (π‘₯𝑑𝑦)))) ↔ (𝐹 ∈ CRing ∧ βˆ€π‘Ÿ ∈ 𝐡 βˆ€π‘₯ ∈ 𝑉 βˆ€π‘¦ ∈ 𝑉 (((π‘Ÿ Β· π‘₯) Γ— 𝑦) = (π‘Ÿ Β· (π‘₯ Γ— 𝑦)) ∧ (π‘₯ Γ— (π‘Ÿ Β· 𝑦)) = (π‘Ÿ Β· (π‘₯ Γ— 𝑦))))))
461, 4, 45sbcied2 3791 . . 3 (𝑀 = π‘Š β†’ ([(Scalarβ€˜π‘€) / 𝑓](𝑓 ∈ CRing ∧ βˆ€π‘Ÿ ∈ (Baseβ€˜π‘“)βˆ€π‘₯ ∈ (Baseβ€˜π‘€)βˆ€π‘¦ ∈ (Baseβ€˜π‘€)[( ·𝑠 β€˜π‘€) / 𝑠][(.rβ€˜π‘€) / 𝑑](((π‘Ÿπ‘ π‘₯)𝑑𝑦) = (π‘Ÿπ‘ (π‘₯𝑑𝑦)) ∧ (π‘₯𝑑(π‘Ÿπ‘ π‘¦)) = (π‘Ÿπ‘ (π‘₯𝑑𝑦)))) ↔ (𝐹 ∈ CRing ∧ βˆ€π‘Ÿ ∈ 𝐡 βˆ€π‘₯ ∈ 𝑉 βˆ€π‘¦ ∈ 𝑉 (((π‘Ÿ Β· π‘₯) Γ— 𝑦) = (π‘Ÿ Β· (π‘₯ Γ— 𝑦)) ∧ (π‘₯ Γ— (π‘Ÿ Β· 𝑦)) = (π‘Ÿ Β· (π‘₯ Γ— 𝑦))))))
47 df-assa 21275 . . 3 AssAlg = {𝑀 ∈ (LMod ∩ Ring) ∣ [(Scalarβ€˜π‘€) / 𝑓](𝑓 ∈ CRing ∧ βˆ€π‘Ÿ ∈ (Baseβ€˜π‘“)βˆ€π‘₯ ∈ (Baseβ€˜π‘€)βˆ€π‘¦ ∈ (Baseβ€˜π‘€)[( ·𝑠 β€˜π‘€) / 𝑠][(.rβ€˜π‘€) / 𝑑](((π‘Ÿπ‘ π‘₯)𝑑𝑦) = (π‘Ÿπ‘ (π‘₯𝑑𝑦)) ∧ (π‘₯𝑑(π‘Ÿπ‘ π‘¦)) = (π‘Ÿπ‘ (π‘₯𝑑𝑦))))}
4846, 47elrab2 3653 . 2 (π‘Š ∈ AssAlg ↔ (π‘Š ∈ (LMod ∩ Ring) ∧ (𝐹 ∈ CRing ∧ βˆ€π‘Ÿ ∈ 𝐡 βˆ€π‘₯ ∈ 𝑉 βˆ€π‘¦ ∈ 𝑉 (((π‘Ÿ Β· π‘₯) Γ— 𝑦) = (π‘Ÿ Β· (π‘₯ Γ— 𝑦)) ∧ (π‘₯ Γ— (π‘Ÿ Β· 𝑦)) = (π‘Ÿ Β· (π‘₯ Γ— 𝑦))))))
49 anass 470 . 2 (((π‘Š ∈ (LMod ∩ Ring) ∧ 𝐹 ∈ CRing) ∧ βˆ€π‘Ÿ ∈ 𝐡 βˆ€π‘₯ ∈ 𝑉 βˆ€π‘¦ ∈ 𝑉 (((π‘Ÿ Β· π‘₯) Γ— 𝑦) = (π‘Ÿ Β· (π‘₯ Γ— 𝑦)) ∧ (π‘₯ Γ— (π‘Ÿ Β· 𝑦)) = (π‘Ÿ Β· (π‘₯ Γ— 𝑦)))) ↔ (π‘Š ∈ (LMod ∩ Ring) ∧ (𝐹 ∈ CRing ∧ βˆ€π‘Ÿ ∈ 𝐡 βˆ€π‘₯ ∈ 𝑉 βˆ€π‘¦ ∈ 𝑉 (((π‘Ÿ Β· π‘₯) Γ— 𝑦) = (π‘Ÿ Β· (π‘₯ Γ— 𝑦)) ∧ (π‘₯ Γ— (π‘Ÿ Β· 𝑦)) = (π‘Ÿ Β· (π‘₯ Γ— 𝑦))))))
50 elin 3931 . . . . 5 (π‘Š ∈ (LMod ∩ Ring) ↔ (π‘Š ∈ LMod ∧ π‘Š ∈ Ring))
5150anbi1i 625 . . . 4 ((π‘Š ∈ (LMod ∩ Ring) ∧ 𝐹 ∈ CRing) ↔ ((π‘Š ∈ LMod ∧ π‘Š ∈ Ring) ∧ 𝐹 ∈ CRing))
52 df-3an 1090 . . . 4 ((π‘Š ∈ LMod ∧ π‘Š ∈ Ring ∧ 𝐹 ∈ CRing) ↔ ((π‘Š ∈ LMod ∧ π‘Š ∈ Ring) ∧ 𝐹 ∈ CRing))
5351, 52bitr4i 278 . . 3 ((π‘Š ∈ (LMod ∩ Ring) ∧ 𝐹 ∈ CRing) ↔ (π‘Š ∈ LMod ∧ π‘Š ∈ Ring ∧ 𝐹 ∈ CRing))
5453anbi1i 625 . 2 (((π‘Š ∈ (LMod ∩ Ring) ∧ 𝐹 ∈ CRing) ∧ βˆ€π‘Ÿ ∈ 𝐡 βˆ€π‘₯ ∈ 𝑉 βˆ€π‘¦ ∈ 𝑉 (((π‘Ÿ Β· π‘₯) Γ— 𝑦) = (π‘Ÿ Β· (π‘₯ Γ— 𝑦)) ∧ (π‘₯ Γ— (π‘Ÿ Β· 𝑦)) = (π‘Ÿ Β· (π‘₯ Γ— 𝑦)))) ↔ ((π‘Š ∈ LMod ∧ π‘Š ∈ Ring ∧ 𝐹 ∈ CRing) ∧ βˆ€π‘Ÿ ∈ 𝐡 βˆ€π‘₯ ∈ 𝑉 βˆ€π‘¦ ∈ 𝑉 (((π‘Ÿ Β· π‘₯) Γ— 𝑦) = (π‘Ÿ Β· (π‘₯ Γ— 𝑦)) ∧ (π‘₯ Γ— (π‘Ÿ Β· 𝑦)) = (π‘Ÿ Β· (π‘₯ Γ— 𝑦)))))
5548, 49, 543bitr2i 299 1 (π‘Š ∈ AssAlg ↔ ((π‘Š ∈ LMod ∧ π‘Š ∈ Ring ∧ 𝐹 ∈ CRing) ∧ βˆ€π‘Ÿ ∈ 𝐡 βˆ€π‘₯ ∈ 𝑉 βˆ€π‘¦ ∈ 𝑉 (((π‘Ÿ Β· π‘₯) Γ— 𝑦) = (π‘Ÿ Β· (π‘₯ Γ— 𝑦)) ∧ (π‘₯ Γ— (π‘Ÿ Β· 𝑦)) = (π‘Ÿ Β· (π‘₯ Γ— 𝑦)))))
Colors of variables: wff setvar class
Syntax hints:   ↔ wb 205   ∧ wa 397   ∧ w3a 1088   = wceq 1542   ∈ wcel 2107  βˆ€wral 3065  Vcvv 3448  [wsbc 3744   ∩ cin 3914  β€˜cfv 6501  (class class class)co 7362  Basecbs 17090  .rcmulr 17141  Scalarcsca 17143   ·𝑠 cvsca 17144  Ringcrg 19971  CRingccrg 19972  LModclmod 20338  AssAlgcasa 21272
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2708  ax-nul 5268
This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1783  df-sb 2069  df-clab 2715  df-cleq 2729  df-clel 2815  df-ne 2945  df-ral 3066  df-rab 3411  df-v 3450  df-sbc 3745  df-dif 3918  df-un 3920  df-in 3922  df-ss 3932  df-nul 4288  df-if 4492  df-sn 4592  df-pr 4594  df-op 4598  df-uni 4871  df-br 5111  df-iota 6453  df-fv 6509  df-ov 7365  df-assa 21275
This theorem is referenced by:  assalem  21279  assalmod  21282  assaring  21283  assasca  21284  isassad  21286  assapropd  21291
  Copyright terms: Public domain W3C validator