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

Metamath Proof Explorer

Theorem drngpropd

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

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

Proof

Step Hyp Ref Expression
1 drngpropd.1 ⊢ ( 𝜑 → 𝐵 = ( Base ‘ 𝐾 ) )
2 drngpropd.2 ⊢ ( 𝜑 → 𝐵 = ( Base ‘ 𝐿 ) )
3 drngpropd.3 ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) → ( 𝑥 ( +g ‘ 𝐾 ) 𝑦 ) = ( 𝑥 ( +g ‘ 𝐿 ) 𝑦 ) )
4 drngpropd.4 ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) → ( 𝑥 ( .r ‘ 𝐾 ) 𝑦 ) = ( 𝑥 ( .r ‘ 𝐿 ) 𝑦 ) )
5 1 2 4 unitpropd ⊢ ( 𝜑 → ( Unit ‘ 𝐾 ) = ( Unit ‘ 𝐿 ) )
6 5 adantr ⊢ ( ( 𝜑 ∧ 𝐾 ∈ Ring ) → ( Unit ‘ 𝐾 ) = ( Unit ‘ 𝐿 ) )
7 1 2 eqtr3d ⊢ ( 𝜑 → ( Base ‘ 𝐾 ) = ( Base ‘ 𝐿 ) )
8 7 adantr ⊢ ( ( 𝜑 ∧ 𝐾 ∈ Ring ) → ( Base ‘ 𝐾 ) = ( Base ‘ 𝐿 ) )
9 1 adantr ⊢ ( ( 𝜑 ∧ 𝐾 ∈ Ring ) → 𝐵 = ( Base ‘ 𝐾 ) )
10 2 adantr ⊢ ( ( 𝜑 ∧ 𝐾 ∈ Ring ) → 𝐵 = ( Base ‘ 𝐿 ) )
11 3 adantlr ⊢ ( ( ( 𝜑 ∧ 𝐾 ∈ Ring ) ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) → ( 𝑥 ( +g ‘ 𝐾 ) 𝑦 ) = ( 𝑥 ( +g ‘ 𝐿 ) 𝑦 ) )
12 9 10 11 grpidpropd ⊢ ( ( 𝜑 ∧ 𝐾 ∈ Ring ) → ( 0g ‘ 𝐾 ) = ( 0g ‘ 𝐿 ) )
13 12 sneqd ⊢ ( ( 𝜑 ∧ 𝐾 ∈ Ring ) → { ( 0g ‘ 𝐾 ) } = { ( 0g ‘ 𝐿 ) } )
14 8 13 difeq12d ⊢ ( ( 𝜑 ∧ 𝐾 ∈ Ring ) → ( ( Base ‘ 𝐾 ) ∖ { ( 0g ‘ 𝐾 ) } ) = ( ( Base ‘ 𝐿 ) ∖ { ( 0g ‘ 𝐿 ) } ) )
15 6 14 eqeq12d ⊢ ( ( 𝜑 ∧ 𝐾 ∈ Ring ) → ( ( Unit ‘ 𝐾 ) = ( ( Base ‘ 𝐾 ) ∖ { ( 0g ‘ 𝐾 ) } ) ↔ ( Unit ‘ 𝐿 ) = ( ( Base ‘ 𝐿 ) ∖ { ( 0g ‘ 𝐿 ) } ) ) )
16 15 pm5.32da ⊢ ( 𝜑 → ( ( 𝐾 ∈ Ring ∧ ( Unit ‘ 𝐾 ) = ( ( Base ‘ 𝐾 ) ∖ { ( 0g ‘ 𝐾 ) } ) ) ↔ ( 𝐾 ∈ Ring ∧ ( Unit ‘ 𝐿 ) = ( ( Base ‘ 𝐿 ) ∖ { ( 0g ‘ 𝐿 ) } ) ) ) )
17 1 2 3 4 ringpropd ⊢ ( 𝜑 → ( 𝐾 ∈ Ring ↔ 𝐿 ∈ Ring ) )
18 17 anbi1d ⊢ ( 𝜑 → ( ( 𝐾 ∈ Ring ∧ ( Unit ‘ 𝐿 ) = ( ( Base ‘ 𝐿 ) ∖ { ( 0g ‘ 𝐿 ) } ) ) ↔ ( 𝐿 ∈ Ring ∧ ( Unit ‘ 𝐿 ) = ( ( Base ‘ 𝐿 ) ∖ { ( 0g ‘ 𝐿 ) } ) ) ) )
19 16 18 bitrd ⊢ ( 𝜑 → ( ( 𝐾 ∈ Ring ∧ ( Unit ‘ 𝐾 ) = ( ( Base ‘ 𝐾 ) ∖ { ( 0g ‘ 𝐾 ) } ) ) ↔ ( 𝐿 ∈ Ring ∧ ( Unit ‘ 𝐿 ) = ( ( Base ‘ 𝐿 ) ∖ { ( 0g ‘ 𝐿 ) } ) ) ) )
20 eqid ⊢ ( Base ‘ 𝐾 ) = ( Base ‘ 𝐾 )
21 eqid ⊢ ( Unit ‘ 𝐾 ) = ( Unit ‘ 𝐾 )
22 eqid ⊢ ( 0g ‘ 𝐾 ) = ( 0g ‘ 𝐾 )
23 20 21 22 isdrng ⊢ ( 𝐾 ∈ DivRing ↔ ( 𝐾 ∈ Ring ∧ ( Unit ‘ 𝐾 ) = ( ( Base ‘ 𝐾 ) ∖ { ( 0g ‘ 𝐾 ) } ) ) )
24 eqid ⊢ ( Base ‘ 𝐿 ) = ( Base ‘ 𝐿 )
25 eqid ⊢ ( Unit ‘ 𝐿 ) = ( Unit ‘ 𝐿 )
26 eqid ⊢ ( 0g ‘ 𝐿 ) = ( 0g ‘ 𝐿 )
27 24 25 26 isdrng ⊢ ( 𝐿 ∈ DivRing ↔ ( 𝐿 ∈ Ring ∧ ( Unit ‘ 𝐿 ) = ( ( Base ‘ 𝐿 ) ∖ { ( 0g ‘ 𝐿 ) } ) ) )
28 19 23 27 3bitr4g ⊢ ( 𝜑 → ( 𝐾 ∈ DivRing ↔ 𝐿 ∈ DivRing ) )