Metamath Proof Explorer


Theorem dvdsr02

Description: Only zero is divisible by zero. (Contributed by Stefan O'Rear, 29-Mar-2015)

Ref Expression
Hypotheses dvdsr0.b B = Base R
dvdsr0.d ˙ = r R
dvdsr0.z 0 ˙ = 0 R
Assertion dvdsr02 R Ring X B 0 ˙ ˙ X X = 0 ˙

Proof

Step Hyp Ref Expression
1 dvdsr0.b B = Base R
2 dvdsr0.d ˙ = r R
3 dvdsr0.z 0 ˙ = 0 R
4 1 3 ring0cl R Ring 0 ˙ B
5 4 adantr R Ring X B 0 ˙ B
6 eqid R = R
7 1 2 6 dvdsr2 0 ˙ B 0 ˙ ˙ X x B x R 0 ˙ = X
8 5 7 syl R Ring X B 0 ˙ ˙ X x B x R 0 ˙ = X
9 1 6 3 ringrz R Ring x B x R 0 ˙ = 0 ˙
10 9 eqeq1d R Ring x B x R 0 ˙ = X 0 ˙ = X
11 eqcom 0 ˙ = X X = 0 ˙
12 10 11 bitrdi R Ring x B x R 0 ˙ = X X = 0 ˙
13 12 rexbidva R Ring x B x R 0 ˙ = X x B X = 0 ˙
14 ringgrp R Ring R Grp
15 1 grpbn0 R Grp B
16 r19.9rzv B X = 0 ˙ x B X = 0 ˙
17 14 15 16 3syl R Ring X = 0 ˙ x B X = 0 ˙
18 13 17 bitr4d R Ring x B x R 0 ˙ = X X = 0 ˙
19 18 adantr R Ring X B x B x R 0 ˙ = X X = 0 ˙
20 8 19 bitrd R Ring X B 0 ˙ ˙ X X = 0 ˙