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 B = Base R
drngid2.t · ˙ = R
drngid2.o 0 ˙ = 0 R
drngid2.u 1 ˙ = 1 R
Assertion drngid2 R DivRing I B I 0 ˙ I · ˙ I = I 1 ˙ = I

Proof

Step Hyp Ref Expression
1 drngid2.b B = Base R
2 drngid2.t · ˙ = R
3 drngid2.o 0 ˙ = 0 R
4 drngid2.u 1 ˙ = 1 R
5 df-3an I B I 0 ˙ I · ˙ I = I I B I 0 ˙ I · ˙ I = I
6 eldifsn I B 0 ˙ I B I 0 ˙
7 6 anbi1i I B 0 ˙ I · ˙ I = I I B I 0 ˙ I · ˙ I = I
8 5 7 bitr4i I B I 0 ˙ I · ˙ I = I I B 0 ˙ I · ˙ I = I
9 eqid mulGrp R 𝑠 B 0 ˙ = mulGrp R 𝑠 B 0 ˙
10 1 3 9 drngmgp R DivRing mulGrp R 𝑠 B 0 ˙ Grp
11 difss B 0 ˙ B
12 eqid mulGrp R = mulGrp R
13 12 1 mgpbas B = Base mulGrp R
14 9 13 ressbas2 B 0 ˙ B B 0 ˙ = Base mulGrp R 𝑠 B 0 ˙
15 11 14 ax-mp B 0 ˙ = Base mulGrp R 𝑠 B 0 ˙
16 1 fvexi B V
17 difexg B V B 0 ˙ V
18 12 2 mgpplusg · ˙ = + mulGrp R
19 9 18 ressplusg B 0 ˙ V · ˙ = + mulGrp R 𝑠 B 0 ˙
20 16 17 19 mp2b · ˙ = + mulGrp R 𝑠 B 0 ˙
21 eqid 0 mulGrp R 𝑠 B 0 ˙ = 0 mulGrp R 𝑠 B 0 ˙
22 15 20 21 isgrpid2 mulGrp R 𝑠 B 0 ˙ Grp I B 0 ˙ I · ˙ I = I 0 mulGrp R 𝑠 B 0 ˙ = I
23 10 22 syl R DivRing I B 0 ˙ I · ˙ I = I 0 mulGrp R 𝑠 B 0 ˙ = I
24 8 23 syl5bb R DivRing I B I 0 ˙ I · ˙ I = I 0 mulGrp R 𝑠 B 0 ˙ = I
25 1 3 4 9 drngid R DivRing 1 ˙ = 0 mulGrp R 𝑠 B 0 ˙
26 25 eqeq1d R DivRing 1 ˙ = I 0 mulGrp R 𝑠 B 0 ˙ = I
27 24 26 bitr4d R DivRing I B I 0 ˙ I · ˙ I = I 1 ˙ = I