Metamath Proof Explorer

Theorem drngid2

Description: Properties showing that an element I is the identity element of a division ring. (Contributed by Mario Carneiro, 11-Oct-2013)

Ref Expression
Hypotheses drngid2.b ⊢ 𝐵 = ( Base ‘ 𝑅 )
drngid2.t ⊢ · = ( .r ‘ 𝑅 )
drngid2.o ⊢ 0 = ( 0g ‘ 𝑅 )
drngid2.u ⊢ 1 = ( 1r ‘ 𝑅 )
Assertion drngid2 ( 𝑅 ∈ DivRing → ( ( 𝐼 ∈ 𝐵 ∧ 𝐼 ≠ 0 ∧ ( 𝐼 · 𝐼 ) = 𝐼 ) ↔ 1 = 𝐼 ) )

Proof

Step Hyp Ref Expression
1 drngid2.b ⊢ 𝐵 = ( Base ‘ 𝑅 )
2 drngid2.t ⊢ · = ( .r ‘ 𝑅 )
3 drngid2.o ⊢ 0 = ( 0g ‘ 𝑅 )
4 drngid2.u ⊢ 1 = ( 1r ‘ 𝑅 )
5 df-3an ⊢ ( ( 𝐼 ∈ 𝐵 ∧ 𝐼 ≠ 0 ∧ ( 𝐼 · 𝐼 ) = 𝐼 ) ↔ ( ( 𝐼 ∈ 𝐵 ∧ 𝐼 ≠ 0 ) ∧ ( 𝐼 · 𝐼 ) = 𝐼 ) )
6 eldifsn ⊢ ( 𝐼 ∈ ( 𝐵 ∖ { 0 } ) ↔ ( 𝐼 ∈ 𝐵 ∧ 𝐼 ≠ 0 ) )
7 6 anbi1i ⊢ ( ( 𝐼 ∈ ( 𝐵 ∖ { 0 } ) ∧ ( 𝐼 · 𝐼 ) = 𝐼 ) ↔ ( ( 𝐼 ∈ 𝐵 ∧ 𝐼 ≠ 0 ) ∧ ( 𝐼 · 𝐼 ) = 𝐼 ) )
8 5 7 bitr4i ⊢ ( ( 𝐼 ∈ 𝐵 ∧ 𝐼 ≠ 0 ∧ ( 𝐼 · 𝐼 ) = 𝐼 ) ↔ ( 𝐼 ∈ ( 𝐵 ∖ { 0 } ) ∧ ( 𝐼 · 𝐼 ) = 𝐼 ) )
9 eqid ⊢ ( ( mulGrp ‘ 𝑅 ) ↾s ( 𝐵 ∖ { 0 } ) ) = ( ( mulGrp ‘ 𝑅 ) ↾s ( 𝐵 ∖ { 0 } ) )
10 1 3 9 drngmgp ⊢ ( 𝑅 ∈ DivRing → ( ( mulGrp ‘ 𝑅 ) ↾s ( 𝐵 ∖ { 0 } ) ) ∈ Grp )
11 difss ⊢ ( 𝐵 ∖ { 0 } ) ⊆ 𝐵
12 eqid ⊢ ( mulGrp ‘ 𝑅 ) = ( mulGrp ‘ 𝑅 )
13 12 1 mgpbas ⊢ 𝐵 = ( Base ‘ ( mulGrp ‘ 𝑅 ) )
14 9 13 ressbas2 ⊢ ( ( 𝐵 ∖ { 0 } ) ⊆ 𝐵 → ( 𝐵 ∖ { 0 } ) = ( Base ‘ ( ( mulGrp ‘ 𝑅 ) ↾s ( 𝐵 ∖ { 0 } ) ) ) )
15 11 14 ax-mp ⊢ ( 𝐵 ∖ { 0 } ) = ( Base ‘ ( ( mulGrp ‘ 𝑅 ) ↾s ( 𝐵 ∖ { 0 } ) ) )
16 1 fvexi ⊢ 𝐵 ∈ V
17 difexg ⊢ ( 𝐵 ∈ V → ( 𝐵 ∖ { 0 } ) ∈ V )
18 12 2 mgpplusg ⊢ · = ( +g ‘ ( mulGrp ‘ 𝑅 ) )
19 9 18 ressplusg ⊢ ( ( 𝐵 ∖ { 0 } ) ∈ V → · = ( +g ‘ ( ( mulGrp ‘ 𝑅 ) ↾s ( 𝐵 ∖ { 0 } ) ) ) )
20 16 17 19 mp2b ⊢ · = ( +g ‘ ( ( mulGrp ‘ 𝑅 ) ↾s ( 𝐵 ∖ { 0 } ) ) )
21 eqid ⊢ ( 0g ‘ ( ( mulGrp ‘ 𝑅 ) ↾s ( 𝐵 ∖ { 0 } ) ) ) = ( 0g ‘ ( ( mulGrp ‘ 𝑅 ) ↾s ( 𝐵 ∖ { 0 } ) ) )
22 15 20 21 isgrpid2 ⊢ ( ( ( mulGrp ‘ 𝑅 ) ↾s ( 𝐵 ∖ { 0 } ) ) ∈ Grp → ( ( 𝐼 ∈ ( 𝐵 ∖ { 0 } ) ∧ ( 𝐼 · 𝐼 ) = 𝐼 ) ↔ ( 0g ‘ ( ( mulGrp ‘ 𝑅 ) ↾s ( 𝐵 ∖ { 0 } ) ) ) = 𝐼 ) )
23 10 22 syl ⊢ ( 𝑅 ∈ DivRing → ( ( 𝐼 ∈ ( 𝐵 ∖ { 0 } ) ∧ ( 𝐼 · 𝐼 ) = 𝐼 ) ↔ ( 0g ‘ ( ( mulGrp ‘ 𝑅 ) ↾s ( 𝐵 ∖ { 0 } ) ) ) = 𝐼 ) )
24 8 23 syl5bb ⊢ ( 𝑅 ∈ DivRing → ( ( 𝐼 ∈ 𝐵 ∧ 𝐼 ≠ 0 ∧ ( 𝐼 · 𝐼 ) = 𝐼 ) ↔ ( 0g ‘ ( ( mulGrp ‘ 𝑅 ) ↾s ( 𝐵 ∖ { 0 } ) ) ) = 𝐼 ) )
25 1 3 4 9 drngid ⊢ ( 𝑅 ∈ DivRing → 1 = ( 0g ‘ ( ( mulGrp ‘ 𝑅 ) ↾s ( 𝐵 ∖ { 0 } ) ) ) )
26 25 eqeq1d ⊢ ( 𝑅 ∈ DivRing → ( 1 = 𝐼 ↔ ( 0g ‘ ( ( mulGrp ‘ 𝑅 ) ↾s ( 𝐵 ∖ { 0 } ) ) ) = 𝐼 ) )
27 24 26 bitr4d ⊢ ( 𝑅 ∈ DivRing → ( ( 𝐼 ∈ 𝐵 ∧ 𝐼 ≠ 0 ∧ ( 𝐼 · 𝐼 ) = 𝐼 ) ↔ 1 = 𝐼 ) )