Metamath Proof Explorer


Theorem zrdivrng

Description: The zero ring is not a division ring. (Contributed by FL, 24-Jan-2010) (Proof shortened by Mario Carneiro, 15-Dec-2013) (New usage is discouraged.)

Ref Expression
Hypothesis zrdivrng.1
|- A e. _V
Assertion zrdivrng
|- -. <. { <. <. A , A >. , A >. } , { <. <. A , A >. , A >. } >. e. DivRingOps

Proof

Step Hyp Ref Expression
1 zrdivrng.1
 |-  A e. _V
2 0ngrp
 |-  -. (/) e. GrpOp
3 opex
 |-  <. A , A >. e. _V
4 3 rnsnop
 |-  ran { <. <. A , A >. , A >. } = { A }
5 1 gidsn
 |-  ( GId ` { <. <. A , A >. , A >. } ) = A
6 5 sneqi
 |-  { ( GId ` { <. <. A , A >. , A >. } ) } = { A }
7 4 6 difeq12i
 |-  ( ran { <. <. A , A >. , A >. } \ { ( GId ` { <. <. A , A >. , A >. } ) } ) = ( { A } \ { A } )
8 difid
 |-  ( { A } \ { A } ) = (/)
9 7 8 eqtri
 |-  ( ran { <. <. A , A >. , A >. } \ { ( GId ` { <. <. A , A >. , A >. } ) } ) = (/)
10 9 xpeq2i
 |-  ( ( ran { <. <. A , A >. , A >. } \ { ( GId ` { <. <. A , A >. , A >. } ) } ) X. ( ran { <. <. A , A >. , A >. } \ { ( GId ` { <. <. A , A >. , A >. } ) } ) ) = ( ( ran { <. <. A , A >. , A >. } \ { ( GId ` { <. <. A , A >. , A >. } ) } ) X. (/) )
11 xp0
 |-  ( ( ran { <. <. A , A >. , A >. } \ { ( GId ` { <. <. A , A >. , A >. } ) } ) X. (/) ) = (/)
12 10 11 eqtri
 |-  ( ( ran { <. <. A , A >. , A >. } \ { ( GId ` { <. <. A , A >. , A >. } ) } ) X. ( ran { <. <. A , A >. , A >. } \ { ( GId ` { <. <. A , A >. , A >. } ) } ) ) = (/)
13 12 reseq2i
 |-  ( { <. <. A , A >. , A >. } |` ( ( ran { <. <. A , A >. , A >. } \ { ( GId ` { <. <. A , A >. , A >. } ) } ) X. ( ran { <. <. A , A >. , A >. } \ { ( GId ` { <. <. A , A >. , A >. } ) } ) ) ) = ( { <. <. A , A >. , A >. } |` (/) )
14 res0
 |-  ( { <. <. A , A >. , A >. } |` (/) ) = (/)
15 13 14 eqtri
 |-  ( { <. <. A , A >. , A >. } |` ( ( ran { <. <. A , A >. , A >. } \ { ( GId ` { <. <. A , A >. , A >. } ) } ) X. ( ran { <. <. A , A >. , A >. } \ { ( GId ` { <. <. A , A >. , A >. } ) } ) ) ) = (/)
16 snex
 |-  { <. <. A , A >. , A >. } e. _V
17 isdivrngo
 |-  ( { <. <. A , A >. , A >. } e. _V -> ( <. { <. <. A , A >. , A >. } , { <. <. A , A >. , A >. } >. e. DivRingOps <-> ( <. { <. <. A , A >. , A >. } , { <. <. A , A >. , A >. } >. e. RingOps /\ ( { <. <. A , A >. , A >. } |` ( ( ran { <. <. A , A >. , A >. } \ { ( GId ` { <. <. A , A >. , A >. } ) } ) X. ( ran { <. <. A , A >. , A >. } \ { ( GId ` { <. <. A , A >. , A >. } ) } ) ) ) e. GrpOp ) ) )
18 16 17 ax-mp
 |-  ( <. { <. <. A , A >. , A >. } , { <. <. A , A >. , A >. } >. e. DivRingOps <-> ( <. { <. <. A , A >. , A >. } , { <. <. A , A >. , A >. } >. e. RingOps /\ ( { <. <. A , A >. , A >. } |` ( ( ran { <. <. A , A >. , A >. } \ { ( GId ` { <. <. A , A >. , A >. } ) } ) X. ( ran { <. <. A , A >. , A >. } \ { ( GId ` { <. <. A , A >. , A >. } ) } ) ) ) e. GrpOp ) )
19 18 simprbi
 |-  ( <. { <. <. A , A >. , A >. } , { <. <. A , A >. , A >. } >. e. DivRingOps -> ( { <. <. A , A >. , A >. } |` ( ( ran { <. <. A , A >. , A >. } \ { ( GId ` { <. <. A , A >. , A >. } ) } ) X. ( ran { <. <. A , A >. , A >. } \ { ( GId ` { <. <. A , A >. , A >. } ) } ) ) ) e. GrpOp )
20 15 19 eqeltrrid
 |-  ( <. { <. <. A , A >. , A >. } , { <. <. A , A >. , A >. } >. e. DivRingOps -> (/) e. GrpOp )
21 2 20 mto
 |-  -. <. { <. <. A , A >. , A >. } , { <. <. A , A >. , A >. } >. e. DivRingOps