Metamath Proof Explorer

Theorem un0mulcl

Description: If S is closed under multiplication, then so is S u. { 0 } . (Contributed by Mario Carneiro, 17-Jul-2014)

Ref Expression
Hypotheses un0addcl.1 
|- ( ph -> S C_ CC )
un0addcl.2 
|- T = ( S u. { 0 } )
un0mulcl.3 
|- ( ( ph /\ ( M e. S /\ N e. S ) ) -> ( M x. N ) e. S )
Assertion un0mulcl 
|- ( ( ph /\ ( M e. T /\ N e. T ) ) -> ( M x. N ) e. T )

Proof

Step Hyp Ref Expression
1 un0addcl.1 
 |-  ( ph -> S C_ CC )
2 un0addcl.2 
 |-  T = ( S u. { 0 } )
3 un0mulcl.3 
 |-  ( ( ph /\ ( M e. S /\ N e. S ) ) -> ( M x. N ) e. S )
4 2 eleq2i 
 |-  ( N e. T <-> N e. ( S u. { 0 } ) )
5 elun 
 |-  ( N e. ( S u. { 0 } ) <-> ( N e. S \/ N e. { 0 } ) )
6 4 5 bitri 
 |-  ( N e. T <-> ( N e. S \/ N e. { 0 } ) )
7 2 eleq2i 
 |-  ( M e. T <-> M e. ( S u. { 0 } ) )
8 elun 
 |-  ( M e. ( S u. { 0 } ) <-> ( M e. S \/ M e. { 0 } ) )
9 7 8 bitri 
 |-  ( M e. T <-> ( M e. S \/ M e. { 0 } ) )
10 ssun1 
 |-  S C_ ( S u. { 0 } )
11 10 2 sseqtrri 
 |-  S C_ T
12 11 3 sseldi 
 |-  ( ( ph /\ ( M e. S /\ N e. S ) ) -> ( M x. N ) e. T )
13 12 expr 
 |-  ( ( ph /\ M e. S ) -> ( N e. S -> ( M x. N ) e. T ) )
14 1 sselda 
 |-  ( ( ph /\ N e. S ) -> N e. CC )
15 14 mul02d 
 |-  ( ( ph /\ N e. S ) -> ( 0 x. N ) = 0 )
16 ssun2 
 |-  { 0 } C_ ( S u. { 0 } )
17 16 2 sseqtrri 
 |-  { 0 } C_ T
18 c0ex 
 |-  0 e. _V
19 18 snss 
 |-  ( 0 e. T <-> { 0 } C_ T )
20 17 19 mpbir 
 |-  0 e. T
21 15 20 eqeltrdi 
 |-  ( ( ph /\ N e. S ) -> ( 0 x. N ) e. T )
22 elsni 
 |-  ( M e. { 0 } -> M = 0 )
23 22 oveq1d 
 |-  ( M e. { 0 } -> ( M x. N ) = ( 0 x. N ) )
24 23 eleq1d 
 |-  ( M e. { 0 } -> ( ( M x. N ) e. T <-> ( 0 x. N ) e. T ) )
25 21 24 syl5ibrcom 
 |-  ( ( ph /\ N e. S ) -> ( M e. { 0 } -> ( M x. N ) e. T ) )
26 25 impancom 
 |-  ( ( ph /\ M e. { 0 } ) -> ( N e. S -> ( M x. N ) e. T ) )
27 13 26 jaodan 
 |-  ( ( ph /\ ( M e. S \/ M e. { 0 } ) ) -> ( N e. S -> ( M x. N ) e. T ) )
28 9 27 sylan2b 
 |-  ( ( ph /\ M e. T ) -> ( N e. S -> ( M x. N ) e. T ) )
29 0cnd 
 |-  ( ph -> 0 e. CC )
30 29 snssd 
 |-  ( ph -> { 0 } C_ CC )
31 1 30 unssd 
 |-  ( ph -> ( S u. { 0 } ) C_ CC )
32 2 31 eqsstrid 
 |-  ( ph -> T C_ CC )
33 32 sselda 
 |-  ( ( ph /\ M e. T ) -> M e. CC )
34 33 mul01d 
 |-  ( ( ph /\ M e. T ) -> ( M x. 0 ) = 0 )
35 34 20 eqeltrdi 
 |-  ( ( ph /\ M e. T ) -> ( M x. 0 ) e. T )
36 elsni 
 |-  ( N e. { 0 } -> N = 0 )
37 36 oveq2d 
 |-  ( N e. { 0 } -> ( M x. N ) = ( M x. 0 ) )
38 37 eleq1d 
 |-  ( N e. { 0 } -> ( ( M x. N ) e. T <-> ( M x. 0 ) e. T ) )
39 35 38 syl5ibrcom 
 |-  ( ( ph /\ M e. T ) -> ( N e. { 0 } -> ( M x. N ) e. T ) )
40 28 39 jaod 
 |-  ( ( ph /\ M e. T ) -> ( ( N e. S \/ N e. { 0 } ) -> ( M x. N ) e. T ) )
41 6 40 syl5bi 
 |-  ( ( ph /\ M e. T ) -> ( N e. T -> ( M x. N ) e. T ) )
42 41 impr 
 |-  ( ( ph /\ ( M e. T /\ N e. T ) ) -> ( M x. N ) e. T )