Metamath Proof Explorer

Theorem ofmulrt

Description: The set of roots of a product is the union of the roots of the terms. (Contributed by Mario Carneiro, 28-Jul-2014)

Ref Expression
Assertion ofmulrt 
|- ( ( A e. V /\ F : A --> CC /\ G : A --> CC ) -> ( `' ( F oF x. G ) " { 0 } ) = ( ( `' F " { 0 } ) u. ( `' G " { 0 } ) ) )

Proof

Step Hyp Ref Expression
1 simp2 
 |-  ( ( A e. V /\ F : A --> CC /\ G : A --> CC ) -> F : A --> CC )
2 1 ffnd 
 |-  ( ( A e. V /\ F : A --> CC /\ G : A --> CC ) -> F Fn A )
3 simp3 
 |-  ( ( A e. V /\ F : A --> CC /\ G : A --> CC ) -> G : A --> CC )
4 3 ffnd 
 |-  ( ( A e. V /\ F : A --> CC /\ G : A --> CC ) -> G Fn A )
5 simp1 
 |-  ( ( A e. V /\ F : A --> CC /\ G : A --> CC ) -> A e. V )
6 inidm 
 |-  ( A i^i A ) = A
7 eqidd 
 |-  ( ( ( A e. V /\ F : A --> CC /\ G : A --> CC ) /\ x e. A ) -> ( F ` x ) = ( F ` x ) )
8 eqidd 
 |-  ( ( ( A e. V /\ F : A --> CC /\ G : A --> CC ) /\ x e. A ) -> ( G ` x ) = ( G ` x ) )
9 2 4 5 5 6 7 8 ofval 
 |-  ( ( ( A e. V /\ F : A --> CC /\ G : A --> CC ) /\ x e. A ) -> ( ( F oF x. G ) ` x ) = ( ( F ` x ) x. ( G ` x ) ) )
10 9 eqeq1d 
 |-  ( ( ( A e. V /\ F : A --> CC /\ G : A --> CC ) /\ x e. A ) -> ( ( ( F oF x. G ) ` x ) = 0 <-> ( ( F ` x ) x. ( G ` x ) ) = 0 ) )
11 1 ffvelrnda 
 |-  ( ( ( A e. V /\ F : A --> CC /\ G : A --> CC ) /\ x e. A ) -> ( F ` x ) e. CC )
12 3 ffvelrnda 
 |-  ( ( ( A e. V /\ F : A --> CC /\ G : A --> CC ) /\ x e. A ) -> ( G ` x ) e. CC )
13 11 12 mul0ord 
 |-  ( ( ( A e. V /\ F : A --> CC /\ G : A --> CC ) /\ x e. A ) -> ( ( ( F ` x ) x. ( G ` x ) ) = 0 <-> ( ( F ` x ) = 0 \/ ( G ` x ) = 0 ) ) )
14 10 13 bitrd 
 |-  ( ( ( A e. V /\ F : A --> CC /\ G : A --> CC ) /\ x e. A ) -> ( ( ( F oF x. G ) ` x ) = 0 <-> ( ( F ` x ) = 0 \/ ( G ` x ) = 0 ) ) )
15 14 pm5.32da 
 |-  ( ( A e. V /\ F : A --> CC /\ G : A --> CC ) -> ( ( x e. A /\ ( ( F oF x. G ) ` x ) = 0 ) <-> ( x e. A /\ ( ( F ` x ) = 0 \/ ( G ` x ) = 0 ) ) ) )
16 2 4 5 5 6 offn 
 |-  ( ( A e. V /\ F : A --> CC /\ G : A --> CC ) -> ( F oF x. G ) Fn A )
17 fniniseg 
 |-  ( ( F oF x. G ) Fn A -> ( x e. ( `' ( F oF x. G ) " { 0 } ) <-> ( x e. A /\ ( ( F oF x. G ) ` x ) = 0 ) ) )
18 16 17 syl 
 |-  ( ( A e. V /\ F : A --> CC /\ G : A --> CC ) -> ( x e. ( `' ( F oF x. G ) " { 0 } ) <-> ( x e. A /\ ( ( F oF x. G ) ` x ) = 0 ) ) )
19 fniniseg 
 |-  ( F Fn A -> ( x e. ( `' F " { 0 } ) <-> ( x e. A /\ ( F ` x ) = 0 ) ) )
20 2 19 syl 
 |-  ( ( A e. V /\ F : A --> CC /\ G : A --> CC ) -> ( x e. ( `' F " { 0 } ) <-> ( x e. A /\ ( F ` x ) = 0 ) ) )
21 fniniseg 
 |-  ( G Fn A -> ( x e. ( `' G " { 0 } ) <-> ( x e. A /\ ( G ` x ) = 0 ) ) )
22 4 21 syl 
 |-  ( ( A e. V /\ F : A --> CC /\ G : A --> CC ) -> ( x e. ( `' G " { 0 } ) <-> ( x e. A /\ ( G ` x ) = 0 ) ) )
23 20 22 orbi12d 
 |-  ( ( A e. V /\ F : A --> CC /\ G : A --> CC ) -> ( ( x e. ( `' F " { 0 } ) \/ x e. ( `' G " { 0 } ) ) <-> ( ( x e. A /\ ( F ` x ) = 0 ) \/ ( x e. A /\ ( G ` x ) = 0 ) ) ) )
24 elun 
 |-  ( x e. ( ( `' F " { 0 } ) u. ( `' G " { 0 } ) ) <-> ( x e. ( `' F " { 0 } ) \/ x e. ( `' G " { 0 } ) ) )
25 andi 
 |-  ( ( x e. A /\ ( ( F ` x ) = 0 \/ ( G ` x ) = 0 ) ) <-> ( ( x e. A /\ ( F ` x ) = 0 ) \/ ( x e. A /\ ( G ` x ) = 0 ) ) )
26 23 24 25 3bitr4g 
 |-  ( ( A e. V /\ F : A --> CC /\ G : A --> CC ) -> ( x e. ( ( `' F " { 0 } ) u. ( `' G " { 0 } ) ) <-> ( x e. A /\ ( ( F ` x ) = 0 \/ ( G ` x ) = 0 ) ) ) )
27 15 18 26 3bitr4d 
 |-  ( ( A e. V /\ F : A --> CC /\ G : A --> CC ) -> ( x e. ( `' ( F oF x. G ) " { 0 } ) <-> x e. ( ( `' F " { 0 } ) u. ( `' G " { 0 } ) ) ) )
28 27 eqrdv 
 |-  ( ( A e. V /\ F : A --> CC /\ G : A --> CC ) -> ( `' ( F oF x. G ) " { 0 } ) = ( ( `' F " { 0 } ) u. ( `' G " { 0 } ) ) )