Metamath Proof Explorer

Theorem drngprop

Description: If two structures have the same ring components (properties), one is a division ring iff the other one is. (Contributed by Mario Carneiro, 11-Oct-2013) (Revised by Mario Carneiro, 28-Dec-2014)

Ref Expression
Hypotheses drngprop.b ⊢ ( Base ‘ 𝐾 ) = ( Base ‘ 𝐿 )
drngprop.p ⊢ ( +g ‘ 𝐾 ) = ( +g ‘ 𝐿 )
drngprop.m ⊢ ( .r ‘ 𝐾 ) = ( .r ‘ 𝐿 )
Assertion drngprop ( 𝐾 ∈ DivRing ↔ 𝐿 ∈ DivRing )

Proof

Step Hyp Ref Expression
1 drngprop.b ⊢ ( Base ‘ 𝐾 ) = ( Base ‘ 𝐿 )
2 drngprop.p ⊢ ( +g ‘ 𝐾 ) = ( +g ‘ 𝐿 )
3 drngprop.m ⊢ ( .r ‘ 𝐾 ) = ( .r ‘ 𝐿 )
4 eqidd ⊢ ( 𝐾 ∈ Ring → ( Base ‘ 𝐾 ) = ( Base ‘ 𝐾 ) )
5 1 a1i ⊢ ( 𝐾 ∈ Ring → ( Base ‘ 𝐾 ) = ( Base ‘ 𝐿 ) )
6 3 oveqi ⊢ ( 𝑥 ( .r ‘ 𝐾 ) 𝑦 ) = ( 𝑥 ( .r ‘ 𝐿 ) 𝑦 )
7 6 a1i ⊢ ( ( 𝐾 ∈ Ring ∧ ( 𝑥 ∈ ( Base ‘ 𝐾 ) ∧ 𝑦 ∈ ( Base ‘ 𝐾 ) ) ) → ( 𝑥 ( .r ‘ 𝐾 ) 𝑦 ) = ( 𝑥 ( .r ‘ 𝐿 ) 𝑦 ) )
8 4 5 7 unitpropd ⊢ ( 𝐾 ∈ Ring → ( Unit ‘ 𝐾 ) = ( Unit ‘ 𝐿 ) )
9 2 oveqi ⊢ ( 𝑥 ( +g ‘ 𝐾 ) 𝑦 ) = ( 𝑥 ( +g ‘ 𝐿 ) 𝑦 )
10 9 a1i ⊢ ( ( 𝐾 ∈ Ring ∧ ( 𝑥 ∈ ( Base ‘ 𝐾 ) ∧ 𝑦 ∈ ( Base ‘ 𝐾 ) ) ) → ( 𝑥 ( +g ‘ 𝐾 ) 𝑦 ) = ( 𝑥 ( +g ‘ 𝐿 ) 𝑦 ) )
11 4 5 10 grpidpropd ⊢ ( 𝐾 ∈ Ring → ( 0g ‘ 𝐾 ) = ( 0g ‘ 𝐿 ) )
12 11 sneqd ⊢ ( 𝐾 ∈ Ring → { ( 0g ‘ 𝐾 ) } = { ( 0g ‘ 𝐿 ) } )
13 12 difeq2d ⊢ ( 𝐾 ∈ Ring → ( ( Base ‘ 𝐾 ) ∖ { ( 0g ‘ 𝐾 ) } ) = ( ( Base ‘ 𝐾 ) ∖ { ( 0g ‘ 𝐿 ) } ) )
14 8 13 eqeq12d ⊢ ( 𝐾 ∈ Ring → ( ( Unit ‘ 𝐾 ) = ( ( Base ‘ 𝐾 ) ∖ { ( 0g ‘ 𝐾 ) } ) ↔ ( Unit ‘ 𝐿 ) = ( ( Base ‘ 𝐾 ) ∖ { ( 0g ‘ 𝐿 ) } ) ) )
15 14 pm5.32i ⊢ ( ( 𝐾 ∈ Ring ∧ ( Unit ‘ 𝐾 ) = ( ( Base ‘ 𝐾 ) ∖ { ( 0g ‘ 𝐾 ) } ) ) ↔ ( 𝐾 ∈ Ring ∧ ( Unit ‘ 𝐿 ) = ( ( Base ‘ 𝐾 ) ∖ { ( 0g ‘ 𝐿 ) } ) ) )
16 1 2 3 ringprop ⊢ ( 𝐾 ∈ Ring ↔ 𝐿 ∈ Ring )
17 16 anbi1i ⊢ ( ( 𝐾 ∈ Ring ∧ ( Unit ‘ 𝐿 ) = ( ( Base ‘ 𝐾 ) ∖ { ( 0g ‘ 𝐿 ) } ) ) ↔ ( 𝐿 ∈ Ring ∧ ( Unit ‘ 𝐿 ) = ( ( Base ‘ 𝐾 ) ∖ { ( 0g ‘ 𝐿 ) } ) ) )
18 15 17 bitri ⊢ ( ( 𝐾 ∈ Ring ∧ ( Unit ‘ 𝐾 ) = ( ( Base ‘ 𝐾 ) ∖ { ( 0g ‘ 𝐾 ) } ) ) ↔ ( 𝐿 ∈ Ring ∧ ( Unit ‘ 𝐿 ) = ( ( Base ‘ 𝐾 ) ∖ { ( 0g ‘ 𝐿 ) } ) ) )
19 eqid ⊢ ( Base ‘ 𝐾 ) = ( Base ‘ 𝐾 )
20 eqid ⊢ ( Unit ‘ 𝐾 ) = ( Unit ‘ 𝐾 )
21 eqid ⊢ ( 0g ‘ 𝐾 ) = ( 0g ‘ 𝐾 )
22 19 20 21 isdrng ⊢ ( 𝐾 ∈ DivRing ↔ ( 𝐾 ∈ Ring ∧ ( Unit ‘ 𝐾 ) = ( ( Base ‘ 𝐾 ) ∖ { ( 0g ‘ 𝐾 ) } ) ) )
23 eqid ⊢ ( Unit ‘ 𝐿 ) = ( Unit ‘ 𝐿 )
24 eqid ⊢ ( 0g ‘ 𝐿 ) = ( 0g ‘ 𝐿 )
25 1 23 24 isdrng ⊢ ( 𝐿 ∈ DivRing ↔ ( 𝐿 ∈ Ring ∧ ( Unit ‘ 𝐿 ) = ( ( Base ‘ 𝐾 ) ∖ { ( 0g ‘ 𝐿 ) } ) ) )
26 18 22 25 3bitr4i ⊢ ( 𝐾 ∈ DivRing ↔ 𝐿 ∈ DivRing )