Metamath Proof Explorer


Theorem crngpropd

Description: If two structures have the same group components (properties), one is a commutative ring iff the other one is. (Contributed by Mario Carneiro, 8-Feb-2015)

Ref Expression
Hypotheses ringpropd.1 ( 𝜑𝐵 = ( Base ‘ 𝐾 ) )
ringpropd.2 ( 𝜑𝐵 = ( Base ‘ 𝐿 ) )
ringpropd.3 ( ( 𝜑 ∧ ( 𝑥𝐵𝑦𝐵 ) ) → ( 𝑥 ( +g𝐾 ) 𝑦 ) = ( 𝑥 ( +g𝐿 ) 𝑦 ) )
ringpropd.4 ( ( 𝜑 ∧ ( 𝑥𝐵𝑦𝐵 ) ) → ( 𝑥 ( .r𝐾 ) 𝑦 ) = ( 𝑥 ( .r𝐿 ) 𝑦 ) )
Assertion crngpropd ( 𝜑 → ( 𝐾 ∈ CRing ↔ 𝐿 ∈ CRing ) )

Proof

Step Hyp Ref Expression
1 ringpropd.1 ( 𝜑𝐵 = ( Base ‘ 𝐾 ) )
2 ringpropd.2 ( 𝜑𝐵 = ( Base ‘ 𝐿 ) )
3 ringpropd.3 ( ( 𝜑 ∧ ( 𝑥𝐵𝑦𝐵 ) ) → ( 𝑥 ( +g𝐾 ) 𝑦 ) = ( 𝑥 ( +g𝐿 ) 𝑦 ) )
4 ringpropd.4 ( ( 𝜑 ∧ ( 𝑥𝐵𝑦𝐵 ) ) → ( 𝑥 ( .r𝐾 ) 𝑦 ) = ( 𝑥 ( .r𝐿 ) 𝑦 ) )
5 1 2 3 4 ringpropd ( 𝜑 → ( 𝐾 ∈ Ring ↔ 𝐿 ∈ Ring ) )
6 eqid ( mulGrp ‘ 𝐾 ) = ( mulGrp ‘ 𝐾 )
7 eqid ( Base ‘ 𝐾 ) = ( Base ‘ 𝐾 )
8 6 7 mgpbas ( Base ‘ 𝐾 ) = ( Base ‘ ( mulGrp ‘ 𝐾 ) )
9 1 8 eqtrdi ( 𝜑𝐵 = ( Base ‘ ( mulGrp ‘ 𝐾 ) ) )
10 eqid ( mulGrp ‘ 𝐿 ) = ( mulGrp ‘ 𝐿 )
11 eqid ( Base ‘ 𝐿 ) = ( Base ‘ 𝐿 )
12 10 11 mgpbas ( Base ‘ 𝐿 ) = ( Base ‘ ( mulGrp ‘ 𝐿 ) )
13 2 12 eqtrdi ( 𝜑𝐵 = ( Base ‘ ( mulGrp ‘ 𝐿 ) ) )
14 eqid ( .r𝐾 ) = ( .r𝐾 )
15 6 14 mgpplusg ( .r𝐾 ) = ( +g ‘ ( mulGrp ‘ 𝐾 ) )
16 15 oveqi ( 𝑥 ( .r𝐾 ) 𝑦 ) = ( 𝑥 ( +g ‘ ( mulGrp ‘ 𝐾 ) ) 𝑦 )
17 eqid ( .r𝐿 ) = ( .r𝐿 )
18 10 17 mgpplusg ( .r𝐿 ) = ( +g ‘ ( mulGrp ‘ 𝐿 ) )
19 18 oveqi ( 𝑥 ( .r𝐿 ) 𝑦 ) = ( 𝑥 ( +g ‘ ( mulGrp ‘ 𝐿 ) ) 𝑦 )
20 4 16 19 3eqtr3g ( ( 𝜑 ∧ ( 𝑥𝐵𝑦𝐵 ) ) → ( 𝑥 ( +g ‘ ( mulGrp ‘ 𝐾 ) ) 𝑦 ) = ( 𝑥 ( +g ‘ ( mulGrp ‘ 𝐿 ) ) 𝑦 ) )
21 9 13 20 cmnpropd ( 𝜑 → ( ( mulGrp ‘ 𝐾 ) ∈ CMnd ↔ ( mulGrp ‘ 𝐿 ) ∈ CMnd ) )
22 5 21 anbi12d ( 𝜑 → ( ( 𝐾 ∈ Ring ∧ ( mulGrp ‘ 𝐾 ) ∈ CMnd ) ↔ ( 𝐿 ∈ Ring ∧ ( mulGrp ‘ 𝐿 ) ∈ CMnd ) ) )
23 6 iscrng ( 𝐾 ∈ CRing ↔ ( 𝐾 ∈ Ring ∧ ( mulGrp ‘ 𝐾 ) ∈ CMnd ) )
24 10 iscrng ( 𝐿 ∈ CRing ↔ ( 𝐿 ∈ Ring ∧ ( mulGrp ‘ 𝐿 ) ∈ CMnd ) )
25 22 23 24 3bitr4g ( 𝜑 → ( 𝐾 ∈ CRing ↔ 𝐿 ∈ CRing ) )