Metamath Proof Explorer


Theorem isdomn3

Description: Nonzero elements form a multiplicative submonoid of any domain. (Contributed by Stefan O'Rear, 11-Sep-2015)

Ref Expression
Hypotheses isdomn3.b B = Base R
isdomn3.z 0 ˙ = 0 R
isdomn3.u U = mulGrp R
Assertion isdomn3 R Domn R Ring B 0 ˙ SubMnd U

Proof

Step Hyp Ref Expression
1 isdomn3.b B = Base R
2 isdomn3.z 0 ˙ = 0 R
3 isdomn3.u U = mulGrp R
4 eqid R = R
5 1 4 2 isdomn R Domn R NzRing x B y B x R y = 0 ˙ x = 0 ˙ y = 0 ˙
6 eqid 1 R = 1 R
7 6 2 isnzr R NzRing R Ring 1 R 0 ˙
8 7 anbi1i R NzRing x B y B x R y = 0 ˙ x = 0 ˙ y = 0 ˙ R Ring 1 R 0 ˙ x B y B x R y = 0 ˙ x = 0 ˙ y = 0 ˙
9 anass R Ring 1 R 0 ˙ x B y B x R y = 0 ˙ x = 0 ˙ y = 0 ˙ R Ring 1 R 0 ˙ x B y B x R y = 0 ˙ x = 0 ˙ y = 0 ˙
10 8 9 bitri R NzRing x B y B x R y = 0 ˙ x = 0 ˙ y = 0 ˙ R Ring 1 R 0 ˙ x B y B x R y = 0 ˙ x = 0 ˙ y = 0 ˙
11 1 6 ringidcl R Ring 1 R B
12 eldifsn 1 R B 0 ˙ 1 R B 1 R 0 ˙
13 12 baibr 1 R B 1 R 0 ˙ 1 R B 0 ˙
14 11 13 syl R Ring 1 R 0 ˙ 1 R B 0 ˙
15 1 4 ringcl R Ring x B y B x R y B
16 15 3expb R Ring x B y B x R y B
17 16 biantrurd R Ring x B y B x R y 0 ˙ x R y B x R y 0 ˙
18 eldifsn x R y B 0 ˙ x R y B x R y 0 ˙
19 17 18 bitr4di R Ring x B y B x R y 0 ˙ x R y B 0 ˙
20 19 imbi2d R Ring x B y B x 0 ˙ y 0 ˙ x R y 0 ˙ x 0 ˙ y 0 ˙ x R y B 0 ˙
21 20 2ralbidva R Ring x B y B x 0 ˙ y 0 ˙ x R y 0 ˙ x B y B x 0 ˙ y 0 ˙ x R y B 0 ˙
22 con34b x R y = 0 ˙ x = 0 ˙ y = 0 ˙ ¬ x = 0 ˙ y = 0 ˙ ¬ x R y = 0 ˙
23 neanior x 0 ˙ y 0 ˙ ¬ x = 0 ˙ y = 0 ˙
24 df-ne x R y 0 ˙ ¬ x R y = 0 ˙
25 23 24 imbi12i x 0 ˙ y 0 ˙ x R y 0 ˙ ¬ x = 0 ˙ y = 0 ˙ ¬ x R y = 0 ˙
26 22 25 bitr4i x R y = 0 ˙ x = 0 ˙ y = 0 ˙ x 0 ˙ y 0 ˙ x R y 0 ˙
27 26 2ralbii x B y B x R y = 0 ˙ x = 0 ˙ y = 0 ˙ x B y B x 0 ˙ y 0 ˙ x R y 0 ˙
28 impexp x B y B x 0 ˙ y 0 ˙ x R y B 0 ˙ x B y B x 0 ˙ y 0 ˙ x R y B 0 ˙
29 an4 x B y B x 0 ˙ y 0 ˙ x B x 0 ˙ y B y 0 ˙
30 eldifsn x B 0 ˙ x B x 0 ˙
31 eldifsn y B 0 ˙ y B y 0 ˙
32 30 31 anbi12i x B 0 ˙ y B 0 ˙ x B x 0 ˙ y B y 0 ˙
33 29 32 bitr4i x B y B x 0 ˙ y 0 ˙ x B 0 ˙ y B 0 ˙
34 33 imbi1i x B y B x 0 ˙ y 0 ˙ x R y B 0 ˙ x B 0 ˙ y B 0 ˙ x R y B 0 ˙
35 28 34 bitr3i x B y B x 0 ˙ y 0 ˙ x R y B 0 ˙ x B 0 ˙ y B 0 ˙ x R y B 0 ˙
36 35 2albii x y x B y B x 0 ˙ y 0 ˙ x R y B 0 ˙ x y x B 0 ˙ y B 0 ˙ x R y B 0 ˙
37 r2al x B y B x 0 ˙ y 0 ˙ x R y B 0 ˙ x y x B y B x 0 ˙ y 0 ˙ x R y B 0 ˙
38 r2al x B 0 ˙ y B 0 ˙ x R y B 0 ˙ x y x B 0 ˙ y B 0 ˙ x R y B 0 ˙
39 36 37 38 3bitr4ri x B 0 ˙ y B 0 ˙ x R y B 0 ˙ x B y B x 0 ˙ y 0 ˙ x R y B 0 ˙
40 21 27 39 3bitr4g R Ring x B y B x R y = 0 ˙ x = 0 ˙ y = 0 ˙ x B 0 ˙ y B 0 ˙ x R y B 0 ˙
41 14 40 anbi12d R Ring 1 R 0 ˙ x B y B x R y = 0 ˙ x = 0 ˙ y = 0 ˙ 1 R B 0 ˙ x B 0 ˙ y B 0 ˙ x R y B 0 ˙
42 3 ringmgp R Ring U Mnd
43 3 1 mgpbas B = Base U
44 3 6 ringidval 1 R = 0 U
45 3 4 mgpplusg R = + U
46 43 44 45 issubm U Mnd B 0 ˙ SubMnd U B 0 ˙ B 1 R B 0 ˙ x B 0 ˙ y B 0 ˙ x R y B 0 ˙
47 3anass B 0 ˙ B 1 R B 0 ˙ x B 0 ˙ y B 0 ˙ x R y B 0 ˙ B 0 ˙ B 1 R B 0 ˙ x B 0 ˙ y B 0 ˙ x R y B 0 ˙
48 46 47 bitrdi U Mnd B 0 ˙ SubMnd U B 0 ˙ B 1 R B 0 ˙ x B 0 ˙ y B 0 ˙ x R y B 0 ˙
49 difss B 0 ˙ B
50 49 biantrur 1 R B 0 ˙ x B 0 ˙ y B 0 ˙ x R y B 0 ˙ B 0 ˙ B 1 R B 0 ˙ x B 0 ˙ y B 0 ˙ x R y B 0 ˙
51 48 50 bitr4di U Mnd B 0 ˙ SubMnd U 1 R B 0 ˙ x B 0 ˙ y B 0 ˙ x R y B 0 ˙
52 42 51 syl R Ring B 0 ˙ SubMnd U 1 R B 0 ˙ x B 0 ˙ y B 0 ˙ x R y B 0 ˙
53 41 52 bitr4d R Ring 1 R 0 ˙ x B y B x R y = 0 ˙ x = 0 ˙ y = 0 ˙ B 0 ˙ SubMnd U
54 53 pm5.32i R Ring 1 R 0 ˙ x B y B x R y = 0 ˙ x = 0 ˙ y = 0 ˙ R Ring B 0 ˙ SubMnd U
55 10 54 bitri R NzRing x B y B x R y = 0 ˙ x = 0 ˙ y = 0 ˙ R Ring B 0 ˙ SubMnd U
56 5 55 bitri R Domn R Ring B 0 ˙ SubMnd U