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

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 ) )