Metamath Proof Explorer

Theorem smu01lem

Description: Lemma for smu01 and smu02 . (Contributed by Mario Carneiro, 19-Sep-2016)

Ref Expression
Hypotheses smu01lem.1 
|- ( ph -> A C_ NN0 )
smu01lem.2 
|- ( ph -> B C_ NN0 )
smu01lem.3 
|- ( ( ph /\ ( k e. NN0 /\ n e. NN0 ) ) -> -. ( k e. A /\ ( n - k ) e. B ) )
Assertion smu01lem 
|- ( ph -> ( A smul B ) = (/) )

Proof

Step Hyp Ref Expression
1 smu01lem.1 
 |-  ( ph -> A C_ NN0 )
2 smu01lem.2 
 |-  ( ph -> B C_ NN0 )
3 smu01lem.3 
 |-  ( ( ph /\ ( k e. NN0 /\ n e. NN0 ) ) -> -. ( k e. A /\ ( n - k ) e. B ) )
4 smucl 
 |-  ( ( A C_ NN0 /\ B C_ NN0 ) -> ( A smul B ) C_ NN0 )
5 1 2 4 syl2anc 
 |-  ( ph -> ( A smul B ) C_ NN0 )
6 5 sseld 
 |-  ( ph -> ( k e. ( A smul B ) -> k e. NN0 ) )
7 noel 
 |-  -. k e. (/)
8 peano2nn0 
 |-  ( k e. NN0 -> ( k + 1 ) e. NN0 )
9 fveqeq2 
 |-  ( x = 0 -> ( ( seq 0 ( ( p e. ~P NN0 , m e. NN0 |-> ( p sadd { n e. NN0 | ( m e. A /\ ( n - m ) e. B ) } ) ) , ( n e. NN0 |-> if ( n = 0 , (/) , ( n - 1 ) ) ) ) ` x ) = (/) <-> ( seq 0 ( ( p e. ~P NN0 , m e. NN0 |-> ( p sadd { n e. NN0 | ( m e. A /\ ( n - m ) e. B ) } ) ) , ( n e. NN0 |-> if ( n = 0 , (/) , ( n - 1 ) ) ) ) ` 0 ) = (/) ) )
10 9 imbi2d 
 |-  ( x = 0 -> ( ( ph -> ( seq 0 ( ( p e. ~P NN0 , m e. NN0 |-> ( p sadd { n e. NN0 | ( m e. A /\ ( n - m ) e. B ) } ) ) , ( n e. NN0 |-> if ( n = 0 , (/) , ( n - 1 ) ) ) ) ` x ) = (/) ) <-> ( ph -> ( seq 0 ( ( p e. ~P NN0 , m e. NN0 |-> ( p sadd { n e. NN0 | ( m e. A /\ ( n - m ) e. B ) } ) ) , ( n e. NN0 |-> if ( n = 0 , (/) , ( n - 1 ) ) ) ) ` 0 ) = (/) ) ) )
11 fveqeq2 
 |-  ( x = k -> ( ( seq 0 ( ( p e. ~P NN0 , m e. NN0 |-> ( p sadd { n e. NN0 | ( m e. A /\ ( n - m ) e. B ) } ) ) , ( n e. NN0 |-> if ( n = 0 , (/) , ( n - 1 ) ) ) ) ` x ) = (/) <-> ( seq 0 ( ( p e. ~P NN0 , m e. NN0 |-> ( p sadd { n e. NN0 | ( m e. A /\ ( n - m ) e. B ) } ) ) , ( n e. NN0 |-> if ( n = 0 , (/) , ( n - 1 ) ) ) ) ` k ) = (/) ) )
12 11 imbi2d 
 |-  ( x = k -> ( ( ph -> ( seq 0 ( ( p e. ~P NN0 , m e. NN0 |-> ( p sadd { n e. NN0 | ( m e. A /\ ( n - m ) e. B ) } ) ) , ( n e. NN0 |-> if ( n = 0 , (/) , ( n - 1 ) ) ) ) ` x ) = (/) ) <-> ( ph -> ( seq 0 ( ( p e. ~P NN0 , m e. NN0 |-> ( p sadd { n e. NN0 | ( m e. A /\ ( n - m ) e. B ) } ) ) , ( n e. NN0 |-> if ( n = 0 , (/) , ( n - 1 ) ) ) ) ` k ) = (/) ) ) )
13 fveqeq2 
 |-  ( x = ( k + 1 ) -> ( ( seq 0 ( ( p e. ~P NN0 , m e. NN0 |-> ( p sadd { n e. NN0 | ( m e. A /\ ( n - m ) e. B ) } ) ) , ( n e. NN0 |-> if ( n = 0 , (/) , ( n - 1 ) ) ) ) ` x ) = (/) <-> ( seq 0 ( ( p e. ~P NN0 , m e. NN0 |-> ( p sadd { n e. NN0 | ( m e. A /\ ( n - m ) e. B ) } ) ) , ( n e. NN0 |-> if ( n = 0 , (/) , ( n - 1 ) ) ) ) ` ( k + 1 ) ) = (/) ) )
14 13 imbi2d 
 |-  ( x = ( k + 1 ) -> ( ( ph -> ( seq 0 ( ( p e. ~P NN0 , m e. NN0 |-> ( p sadd { n e. NN0 | ( m e. A /\ ( n - m ) e. B ) } ) ) , ( n e. NN0 |-> if ( n = 0 , (/) , ( n - 1 ) ) ) ) ` x ) = (/) ) <-> ( ph -> ( seq 0 ( ( p e. ~P NN0 , m e. NN0 |-> ( p sadd { n e. NN0 | ( m e. A /\ ( n - m ) e. B ) } ) ) , ( n e. NN0 |-> if ( n = 0 , (/) , ( n - 1 ) ) ) ) ` ( k + 1 ) ) = (/) ) ) )
15 eqid 
 |-  seq 0 ( ( p e. ~P NN0 , m e. NN0 |-> ( p sadd { n e. NN0 | ( m e. A /\ ( n - m ) e. B ) } ) ) , ( n e. NN0 |-> if ( n = 0 , (/) , ( n - 1 ) ) ) ) = seq 0 ( ( p e. ~P NN0 , m e. NN0 |-> ( p sadd { n e. NN0 | ( m e. A /\ ( n - m ) e. B ) } ) ) , ( n e. NN0 |-> if ( n = 0 , (/) , ( n - 1 ) ) ) )
16 1 2 15 smup0 
 |-  ( ph -> ( seq 0 ( ( p e. ~P NN0 , m e. NN0 |-> ( p sadd { n e. NN0 | ( m e. A /\ ( n - m ) e. B ) } ) ) , ( n e. NN0 |-> if ( n = 0 , (/) , ( n - 1 ) ) ) ) ` 0 ) = (/) )
17 oveq1 
 |-  ( ( seq 0 ( ( p e. ~P NN0 , m e. NN0 |-> ( p sadd { n e. NN0 | ( m e. A /\ ( n - m ) e. B ) } ) ) , ( n e. NN0 |-> if ( n = 0 , (/) , ( n - 1 ) ) ) ) ` k ) = (/) -> ( ( seq 0 ( ( p e. ~P NN0 , m e. NN0 |-> ( p sadd { n e. NN0 | ( m e. A /\ ( n - m ) e. B ) } ) ) , ( n e. NN0 |-> if ( n = 0 , (/) , ( n - 1 ) ) ) ) ` k ) sadd { n e. NN0 | ( k e. A /\ ( n - k ) e. B ) } ) = ( (/) sadd { n e. NN0 | ( k e. A /\ ( n - k ) e. B ) } ) )
18 1 adantr 
 |-  ( ( ph /\ k e. NN0 ) -> A C_ NN0 )
19 2 adantr 
 |-  ( ( ph /\ k e. NN0 ) -> B C_ NN0 )
20 simpr 
 |-  ( ( ph /\ k e. NN0 ) -> k e. NN0 )
21 18 19 15 20 smupp1 
 |-  ( ( ph /\ k e. NN0 ) -> ( seq 0 ( ( p e. ~P NN0 , m e. NN0 |-> ( p sadd { n e. NN0 | ( m e. A /\ ( n - m ) e. B ) } ) ) , ( n e. NN0 |-> if ( n = 0 , (/) , ( n - 1 ) ) ) ) ` ( k + 1 ) ) = ( ( seq 0 ( ( p e. ~P NN0 , m e. NN0 |-> ( p sadd { n e. NN0 | ( m e. A /\ ( n - m ) e. B ) } ) ) , ( n e. NN0 |-> if ( n = 0 , (/) , ( n - 1 ) ) ) ) ` k ) sadd { n e. NN0 | ( k e. A /\ ( n - k ) e. B ) } ) )
22 3 anassrs 
 |-  ( ( ( ph /\ k e. NN0 ) /\ n e. NN0 ) -> -. ( k e. A /\ ( n - k ) e. B ) )
23 22 ralrimiva 
 |-  ( ( ph /\ k e. NN0 ) -> A. n e. NN0 -. ( k e. A /\ ( n - k ) e. B ) )
24 rabeq0 
 |-  ( { n e. NN0 | ( k e. A /\ ( n - k ) e. B ) } = (/) <-> A. n e. NN0 -. ( k e. A /\ ( n - k ) e. B ) )
25 23 24 sylibr 
 |-  ( ( ph /\ k e. NN0 ) -> { n e. NN0 | ( k e. A /\ ( n - k ) e. B ) } = (/) )
26 25 oveq2d 
 |-  ( ( ph /\ k e. NN0 ) -> ( (/) sadd { n e. NN0 | ( k e. A /\ ( n - k ) e. B ) } ) = ( (/) sadd (/) ) )
27 0ss 
 |-  (/) C_ NN0
28 sadid1 
 |-  ( (/) C_ NN0 -> ( (/) sadd (/) ) = (/) )
29 27 28 mp1i 
 |-  ( ( ph /\ k e. NN0 ) -> ( (/) sadd (/) ) = (/) )
30 26 29 eqtr2d 
 |-  ( ( ph /\ k e. NN0 ) -> (/) = ( (/) sadd { n e. NN0 | ( k e. A /\ ( n - k ) e. B ) } ) )
31 21 30 eqeq12d 
 |-  ( ( ph /\ k e. NN0 ) -> ( ( seq 0 ( ( p e. ~P NN0 , m e. NN0 |-> ( p sadd { n e. NN0 | ( m e. A /\ ( n - m ) e. B ) } ) ) , ( n e. NN0 |-> if ( n = 0 , (/) , ( n - 1 ) ) ) ) ` ( k + 1 ) ) = (/) <-> ( ( seq 0 ( ( p e. ~P NN0 , m e. NN0 |-> ( p sadd { n e. NN0 | ( m e. A /\ ( n - m ) e. B ) } ) ) , ( n e. NN0 |-> if ( n = 0 , (/) , ( n - 1 ) ) ) ) ` k ) sadd { n e. NN0 | ( k e. A /\ ( n - k ) e. B ) } ) = ( (/) sadd { n e. NN0 | ( k e. A /\ ( n - k ) e. B ) } ) ) )
32 17 31 syl5ibr 
 |-  ( ( ph /\ k e. NN0 ) -> ( ( seq 0 ( ( p e. ~P NN0 , m e. NN0 |-> ( p sadd { n e. NN0 | ( m e. A /\ ( n - m ) e. B ) } ) ) , ( n e. NN0 |-> if ( n = 0 , (/) , ( n - 1 ) ) ) ) ` k ) = (/) -> ( seq 0 ( ( p e. ~P NN0 , m e. NN0 |-> ( p sadd { n e. NN0 | ( m e. A /\ ( n - m ) e. B ) } ) ) , ( n e. NN0 |-> if ( n = 0 , (/) , ( n - 1 ) ) ) ) ` ( k + 1 ) ) = (/) ) )
33 32 expcom 
 |-  ( k e. NN0 -> ( ph -> ( ( seq 0 ( ( p e. ~P NN0 , m e. NN0 |-> ( p sadd { n e. NN0 | ( m e. A /\ ( n - m ) e. B ) } ) ) , ( n e. NN0 |-> if ( n = 0 , (/) , ( n - 1 ) ) ) ) ` k ) = (/) -> ( seq 0 ( ( p e. ~P NN0 , m e. NN0 |-> ( p sadd { n e. NN0 | ( m e. A /\ ( n - m ) e. B ) } ) ) , ( n e. NN0 |-> if ( n = 0 , (/) , ( n - 1 ) ) ) ) ` ( k + 1 ) ) = (/) ) ) )
34 33 a2d 
 |-  ( k e. NN0 -> ( ( ph -> ( seq 0 ( ( p e. ~P NN0 , m e. NN0 |-> ( p sadd { n e. NN0 | ( m e. A /\ ( n - m ) e. B ) } ) ) , ( n e. NN0 |-> if ( n = 0 , (/) , ( n - 1 ) ) ) ) ` k ) = (/) ) -> ( ph -> ( seq 0 ( ( p e. ~P NN0 , m e. NN0 |-> ( p sadd { n e. NN0 | ( m e. A /\ ( n - m ) e. B ) } ) ) , ( n e. NN0 |-> if ( n = 0 , (/) , ( n - 1 ) ) ) ) ` ( k + 1 ) ) = (/) ) ) )
35 10 12 14 14 16 34 nn0ind 
 |-  ( ( k + 1 ) e. NN0 -> ( ph -> ( seq 0 ( ( p e. ~P NN0 , m e. NN0 |-> ( p sadd { n e. NN0 | ( m e. A /\ ( n - m ) e. B ) } ) ) , ( n e. NN0 |-> if ( n = 0 , (/) , ( n - 1 ) ) ) ) ` ( k + 1 ) ) = (/) ) )
36 8 35 syl 
 |-  ( k e. NN0 -> ( ph -> ( seq 0 ( ( p e. ~P NN0 , m e. NN0 |-> ( p sadd { n e. NN0 | ( m e. A /\ ( n - m ) e. B ) } ) ) , ( n e. NN0 |-> if ( n = 0 , (/) , ( n - 1 ) ) ) ) ` ( k + 1 ) ) = (/) ) )
37 36 impcom 
 |-  ( ( ph /\ k e. NN0 ) -> ( seq 0 ( ( p e. ~P NN0 , m e. NN0 |-> ( p sadd { n e. NN0 | ( m e. A /\ ( n - m ) e. B ) } ) ) , ( n e. NN0 |-> if ( n = 0 , (/) , ( n - 1 ) ) ) ) ` ( k + 1 ) ) = (/) )
38 37 eleq2d 
 |-  ( ( ph /\ k e. NN0 ) -> ( k e. ( seq 0 ( ( p e. ~P NN0 , m e. NN0 |-> ( p sadd { n e. NN0 | ( m e. A /\ ( n - m ) e. B ) } ) ) , ( n e. NN0 |-> if ( n = 0 , (/) , ( n - 1 ) ) ) ) ` ( k + 1 ) ) <-> k e. (/) ) )
39 7 38 mtbiri 
 |-  ( ( ph /\ k e. NN0 ) -> -. k e. ( seq 0 ( ( p e. ~P NN0 , m e. NN0 |-> ( p sadd { n e. NN0 | ( m e. A /\ ( n - m ) e. B ) } ) ) , ( n e. NN0 |-> if ( n = 0 , (/) , ( n - 1 ) ) ) ) ` ( k + 1 ) ) )
40 18 19 15 20 smuval 
 |-  ( ( ph /\ k e. NN0 ) -> ( k e. ( A smul B ) <-> k e. ( seq 0 ( ( p e. ~P NN0 , m e. NN0 |-> ( p sadd { n e. NN0 | ( m e. A /\ ( n - m ) e. B ) } ) ) , ( n e. NN0 |-> if ( n = 0 , (/) , ( n - 1 ) ) ) ) ` ( k + 1 ) ) ) )
41 39 40 mtbird 
 |-  ( ( ph /\ k e. NN0 ) -> -. k e. ( A smul B ) )
42 41 ex 
 |-  ( ph -> ( k e. NN0 -> -. k e. ( A smul B ) ) )
43 6 42 syld 
 |-  ( ph -> ( k e. ( A smul B ) -> -. k e. ( A smul B ) ) )
44 43 pm2.01d 
 |-  ( ph -> -. k e. ( A smul B ) )
45 44 eq0rdv 
 |-  ( ph -> ( A smul B ) = (/) )