Step |
Hyp |
Ref |
Expression |
1 |
|
fsuppunbi.u |
|- ( ph -> Fun ( F u. G ) ) |
2 |
|
relfsupp |
|- Rel finSupp |
3 |
2
|
brrelex12i |
|- ( ( F u. G ) finSupp Z -> ( ( F u. G ) e. _V /\ Z e. _V ) ) |
4 |
|
unexb |
|- ( ( F e. _V /\ G e. _V ) <-> ( F u. G ) e. _V ) |
5 |
|
simpr |
|- ( ( Fun ( F u. G ) /\ ( ( F u. G ) supp Z ) e. Fin ) -> ( ( F u. G ) supp Z ) e. Fin ) |
6 |
5
|
adantr |
|- ( ( ( Fun ( F u. G ) /\ ( ( F u. G ) supp Z ) e. Fin ) /\ ( ( F e. _V /\ G e. _V ) /\ Z e. _V ) ) -> ( ( F u. G ) supp Z ) e. Fin ) |
7 |
|
simprlr |
|- ( ( ( Fun ( F u. G ) /\ ( ( F u. G ) supp Z ) e. Fin ) /\ ( ( F e. _V /\ G e. _V ) /\ Z e. _V ) ) -> G e. _V ) |
8 |
7
|
suppun |
|- ( ( ( Fun ( F u. G ) /\ ( ( F u. G ) supp Z ) e. Fin ) /\ ( ( F e. _V /\ G e. _V ) /\ Z e. _V ) ) -> ( F supp Z ) C_ ( ( F u. G ) supp Z ) ) |
9 |
6 8
|
ssfid |
|- ( ( ( Fun ( F u. G ) /\ ( ( F u. G ) supp Z ) e. Fin ) /\ ( ( F e. _V /\ G e. _V ) /\ Z e. _V ) ) -> ( F supp Z ) e. Fin ) |
10 |
|
fununfun |
|- ( Fun ( F u. G ) -> ( Fun F /\ Fun G ) ) |
11 |
10
|
simpld |
|- ( Fun ( F u. G ) -> Fun F ) |
12 |
11
|
adantr |
|- ( ( Fun ( F u. G ) /\ ( ( F u. G ) supp Z ) e. Fin ) -> Fun F ) |
13 |
12
|
adantr |
|- ( ( ( Fun ( F u. G ) /\ ( ( F u. G ) supp Z ) e. Fin ) /\ ( ( F e. _V /\ G e. _V ) /\ Z e. _V ) ) -> Fun F ) |
14 |
|
simprll |
|- ( ( ( Fun ( F u. G ) /\ ( ( F u. G ) supp Z ) e. Fin ) /\ ( ( F e. _V /\ G e. _V ) /\ Z e. _V ) ) -> F e. _V ) |
15 |
|
simpr |
|- ( ( ( F e. _V /\ G e. _V ) /\ Z e. _V ) -> Z e. _V ) |
16 |
15
|
adantl |
|- ( ( ( Fun ( F u. G ) /\ ( ( F u. G ) supp Z ) e. Fin ) /\ ( ( F e. _V /\ G e. _V ) /\ Z e. _V ) ) -> Z e. _V ) |
17 |
|
funisfsupp |
|- ( ( Fun F /\ F e. _V /\ Z e. _V ) -> ( F finSupp Z <-> ( F supp Z ) e. Fin ) ) |
18 |
13 14 16 17
|
syl3anc |
|- ( ( ( Fun ( F u. G ) /\ ( ( F u. G ) supp Z ) e. Fin ) /\ ( ( F e. _V /\ G e. _V ) /\ Z e. _V ) ) -> ( F finSupp Z <-> ( F supp Z ) e. Fin ) ) |
19 |
9 18
|
mpbird |
|- ( ( ( Fun ( F u. G ) /\ ( ( F u. G ) supp Z ) e. Fin ) /\ ( ( F e. _V /\ G e. _V ) /\ Z e. _V ) ) -> F finSupp Z ) |
20 |
|
uncom |
|- ( F u. G ) = ( G u. F ) |
21 |
20
|
oveq1i |
|- ( ( F u. G ) supp Z ) = ( ( G u. F ) supp Z ) |
22 |
21
|
eleq1i |
|- ( ( ( F u. G ) supp Z ) e. Fin <-> ( ( G u. F ) supp Z ) e. Fin ) |
23 |
22
|
biimpi |
|- ( ( ( F u. G ) supp Z ) e. Fin -> ( ( G u. F ) supp Z ) e. Fin ) |
24 |
23
|
adantl |
|- ( ( Fun ( F u. G ) /\ ( ( F u. G ) supp Z ) e. Fin ) -> ( ( G u. F ) supp Z ) e. Fin ) |
25 |
24
|
adantr |
|- ( ( ( Fun ( F u. G ) /\ ( ( F u. G ) supp Z ) e. Fin ) /\ ( ( F e. _V /\ G e. _V ) /\ Z e. _V ) ) -> ( ( G u. F ) supp Z ) e. Fin ) |
26 |
14
|
suppun |
|- ( ( ( Fun ( F u. G ) /\ ( ( F u. G ) supp Z ) e. Fin ) /\ ( ( F e. _V /\ G e. _V ) /\ Z e. _V ) ) -> ( G supp Z ) C_ ( ( G u. F ) supp Z ) ) |
27 |
25 26
|
ssfid |
|- ( ( ( Fun ( F u. G ) /\ ( ( F u. G ) supp Z ) e. Fin ) /\ ( ( F e. _V /\ G e. _V ) /\ Z e. _V ) ) -> ( G supp Z ) e. Fin ) |
28 |
10
|
simprd |
|- ( Fun ( F u. G ) -> Fun G ) |
29 |
28
|
adantr |
|- ( ( Fun ( F u. G ) /\ ( ( F u. G ) supp Z ) e. Fin ) -> Fun G ) |
30 |
29
|
adantr |
|- ( ( ( Fun ( F u. G ) /\ ( ( F u. G ) supp Z ) e. Fin ) /\ ( ( F e. _V /\ G e. _V ) /\ Z e. _V ) ) -> Fun G ) |
31 |
|
funisfsupp |
|- ( ( Fun G /\ G e. _V /\ Z e. _V ) -> ( G finSupp Z <-> ( G supp Z ) e. Fin ) ) |
32 |
30 7 16 31
|
syl3anc |
|- ( ( ( Fun ( F u. G ) /\ ( ( F u. G ) supp Z ) e. Fin ) /\ ( ( F e. _V /\ G e. _V ) /\ Z e. _V ) ) -> ( G finSupp Z <-> ( G supp Z ) e. Fin ) ) |
33 |
27 32
|
mpbird |
|- ( ( ( Fun ( F u. G ) /\ ( ( F u. G ) supp Z ) e. Fin ) /\ ( ( F e. _V /\ G e. _V ) /\ Z e. _V ) ) -> G finSupp Z ) |
34 |
19 33
|
jca |
|- ( ( ( Fun ( F u. G ) /\ ( ( F u. G ) supp Z ) e. Fin ) /\ ( ( F e. _V /\ G e. _V ) /\ Z e. _V ) ) -> ( F finSupp Z /\ G finSupp Z ) ) |
35 |
34
|
a1d |
|- ( ( ( Fun ( F u. G ) /\ ( ( F u. G ) supp Z ) e. Fin ) /\ ( ( F e. _V /\ G e. _V ) /\ Z e. _V ) ) -> ( ph -> ( F finSupp Z /\ G finSupp Z ) ) ) |
36 |
35
|
ex |
|- ( ( Fun ( F u. G ) /\ ( ( F u. G ) supp Z ) e. Fin ) -> ( ( ( F e. _V /\ G e. _V ) /\ Z e. _V ) -> ( ph -> ( F finSupp Z /\ G finSupp Z ) ) ) ) |
37 |
|
fsuppimp |
|- ( ( F u. G ) finSupp Z -> ( Fun ( F u. G ) /\ ( ( F u. G ) supp Z ) e. Fin ) ) |
38 |
36 37
|
syl11 |
|- ( ( ( F e. _V /\ G e. _V ) /\ Z e. _V ) -> ( ( F u. G ) finSupp Z -> ( ph -> ( F finSupp Z /\ G finSupp Z ) ) ) ) |
39 |
4 38
|
sylanbr |
|- ( ( ( F u. G ) e. _V /\ Z e. _V ) -> ( ( F u. G ) finSupp Z -> ( ph -> ( F finSupp Z /\ G finSupp Z ) ) ) ) |
40 |
3 39
|
mpcom |
|- ( ( F u. G ) finSupp Z -> ( ph -> ( F finSupp Z /\ G finSupp Z ) ) ) |
41 |
40
|
com12 |
|- ( ph -> ( ( F u. G ) finSupp Z -> ( F finSupp Z /\ G finSupp Z ) ) ) |
42 |
|
simpl |
|- ( ( F finSupp Z /\ G finSupp Z ) -> F finSupp Z ) |
43 |
|
simpr |
|- ( ( F finSupp Z /\ G finSupp Z ) -> G finSupp Z ) |
44 |
42 43
|
fsuppun |
|- ( ( F finSupp Z /\ G finSupp Z ) -> ( ( F u. G ) supp Z ) e. Fin ) |
45 |
44
|
adantl |
|- ( ( ph /\ ( F finSupp Z /\ G finSupp Z ) ) -> ( ( F u. G ) supp Z ) e. Fin ) |
46 |
1
|
adantr |
|- ( ( ph /\ ( F finSupp Z /\ G finSupp Z ) ) -> Fun ( F u. G ) ) |
47 |
2
|
brrelex1i |
|- ( F finSupp Z -> F e. _V ) |
48 |
2
|
brrelex1i |
|- ( G finSupp Z -> G e. _V ) |
49 |
|
unexg |
|- ( ( F e. _V /\ G e. _V ) -> ( F u. G ) e. _V ) |
50 |
47 48 49
|
syl2an |
|- ( ( F finSupp Z /\ G finSupp Z ) -> ( F u. G ) e. _V ) |
51 |
50
|
adantl |
|- ( ( ph /\ ( F finSupp Z /\ G finSupp Z ) ) -> ( F u. G ) e. _V ) |
52 |
2
|
brrelex2i |
|- ( F finSupp Z -> Z e. _V ) |
53 |
52
|
adantr |
|- ( ( F finSupp Z /\ G finSupp Z ) -> Z e. _V ) |
54 |
53
|
adantl |
|- ( ( ph /\ ( F finSupp Z /\ G finSupp Z ) ) -> Z e. _V ) |
55 |
|
funisfsupp |
|- ( ( Fun ( F u. G ) /\ ( F u. G ) e. _V /\ Z e. _V ) -> ( ( F u. G ) finSupp Z <-> ( ( F u. G ) supp Z ) e. Fin ) ) |
56 |
46 51 54 55
|
syl3anc |
|- ( ( ph /\ ( F finSupp Z /\ G finSupp Z ) ) -> ( ( F u. G ) finSupp Z <-> ( ( F u. G ) supp Z ) e. Fin ) ) |
57 |
45 56
|
mpbird |
|- ( ( ph /\ ( F finSupp Z /\ G finSupp Z ) ) -> ( F u. G ) finSupp Z ) |
58 |
57
|
ex |
|- ( ph -> ( ( F finSupp Z /\ G finSupp Z ) -> ( F u. G ) finSupp Z ) ) |
59 |
41 58
|
impbid |
|- ( ph -> ( ( F u. G ) finSupp Z <-> ( F finSupp Z /\ G finSupp Z ) ) ) |