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	⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐹 : 𝐴 ⟶ ℂ ∧ 𝐺 : 𝐴 ⟶ ℂ ) → ( ◡ ( 𝐹 ∘f · 𝐺 ) “ { 0 } ) = ( ( ◡ 𝐹 “ { 0 } ) ∪ ( ◡ 𝐺 “ { 0 } ) ) )

Proof

Step	Hyp	Ref	Expression
1		simp2	⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐹 : 𝐴 ⟶ ℂ ∧ 𝐺 : 𝐴 ⟶ ℂ ) → 𝐹 : 𝐴 ⟶ ℂ )
2	1	ffnd	⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐹 : 𝐴 ⟶ ℂ ∧ 𝐺 : 𝐴 ⟶ ℂ ) → 𝐹 Fn 𝐴 )
3		simp3	⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐹 : 𝐴 ⟶ ℂ ∧ 𝐺 : 𝐴 ⟶ ℂ ) → 𝐺 : 𝐴 ⟶ ℂ )
4	3	ffnd	⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐹 : 𝐴 ⟶ ℂ ∧ 𝐺 : 𝐴 ⟶ ℂ ) → 𝐺 Fn 𝐴 )
5		simp1	⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐹 : 𝐴 ⟶ ℂ ∧ 𝐺 : 𝐴 ⟶ ℂ ) → 𝐴 ∈ 𝑉 )
6		inidm	⊢ ( 𝐴 ∩ 𝐴 ) = 𝐴
7		eqidd	⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐹 : 𝐴 ⟶ ℂ ∧ 𝐺 : 𝐴 ⟶ ℂ ) ∧ 𝑥 ∈ 𝐴 ) → ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑥 ) )
8		eqidd	⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐹 : 𝐴 ⟶ ℂ ∧ 𝐺 : 𝐴 ⟶ ℂ ) ∧ 𝑥 ∈ 𝐴 ) → ( 𝐺 ‘ 𝑥 ) = ( 𝐺 ‘ 𝑥 ) )
9	2 4 5 5 6 7 8	ofval	⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐹 : 𝐴 ⟶ ℂ ∧ 𝐺 : 𝐴 ⟶ ℂ ) ∧ 𝑥 ∈ 𝐴 ) → ( ( 𝐹 ∘f · 𝐺 ) ‘ 𝑥 ) = ( ( 𝐹 ‘ 𝑥 ) · ( 𝐺 ‘ 𝑥 ) ) )
10	9	eqeq1d	⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐹 : 𝐴 ⟶ ℂ ∧ 𝐺 : 𝐴 ⟶ ℂ ) ∧ 𝑥 ∈ 𝐴 ) → ( ( ( 𝐹 ∘f · 𝐺 ) ‘ 𝑥 ) = 0 ↔ ( ( 𝐹 ‘ 𝑥 ) · ( 𝐺 ‘ 𝑥 ) ) = 0 ) )
11	1	ffvelcdmda	⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐹 : 𝐴 ⟶ ℂ ∧ 𝐺 : 𝐴 ⟶ ℂ ) ∧ 𝑥 ∈ 𝐴 ) → ( 𝐹 ‘ 𝑥 ) ∈ ℂ )
12	3	ffvelcdmda	⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐹 : 𝐴 ⟶ ℂ ∧ 𝐺 : 𝐴 ⟶ ℂ ) ∧ 𝑥 ∈ 𝐴 ) → ( 𝐺 ‘ 𝑥 ) ∈ ℂ )
13	11 12	mul0ord	⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐹 : 𝐴 ⟶ ℂ ∧ 𝐺 : 𝐴 ⟶ ℂ ) ∧ 𝑥 ∈ 𝐴 ) → ( ( ( 𝐹 ‘ 𝑥 ) · ( 𝐺 ‘ 𝑥 ) ) = 0 ↔ ( ( 𝐹 ‘ 𝑥 ) = 0 ∨ ( 𝐺 ‘ 𝑥 ) = 0 ) ) )
14	10 13	bitrd	⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐹 : 𝐴 ⟶ ℂ ∧ 𝐺 : 𝐴 ⟶ ℂ ) ∧ 𝑥 ∈ 𝐴 ) → ( ( ( 𝐹 ∘f · 𝐺 ) ‘ 𝑥 ) = 0 ↔ ( ( 𝐹 ‘ 𝑥 ) = 0 ∨ ( 𝐺 ‘ 𝑥 ) = 0 ) ) )
15	14	pm5.32da	⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐹 : 𝐴 ⟶ ℂ ∧ 𝐺 : 𝐴 ⟶ ℂ ) → ( ( 𝑥 ∈ 𝐴 ∧ ( ( 𝐹 ∘f · 𝐺 ) ‘ 𝑥 ) = 0 ) ↔ ( 𝑥 ∈ 𝐴 ∧ ( ( 𝐹 ‘ 𝑥 ) = 0 ∨ ( 𝐺 ‘ 𝑥 ) = 0 ) ) ) )
16	2 4 5 5 6	offn	⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐹 : 𝐴 ⟶ ℂ ∧ 𝐺 : 𝐴 ⟶ ℂ ) → ( 𝐹 ∘f · 𝐺 ) Fn 𝐴 )
17		fniniseg	⊢ ( ( 𝐹 ∘f · 𝐺 ) Fn 𝐴 → ( 𝑥 ∈ ( ◡ ( 𝐹 ∘f · 𝐺 ) “ { 0 } ) ↔ ( 𝑥 ∈ 𝐴 ∧ ( ( 𝐹 ∘f · 𝐺 ) ‘ 𝑥 ) = 0 ) ) )
18	16 17	syl	⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐹 : 𝐴 ⟶ ℂ ∧ 𝐺 : 𝐴 ⟶ ℂ ) → ( 𝑥 ∈ ( ◡ ( 𝐹 ∘f · 𝐺 ) “ { 0 } ) ↔ ( 𝑥 ∈ 𝐴 ∧ ( ( 𝐹 ∘f · 𝐺 ) ‘ 𝑥 ) = 0 ) ) )
19		fniniseg	⊢ ( 𝐹 Fn 𝐴 → ( 𝑥 ∈ ( ◡ 𝐹 “ { 0 } ) ↔ ( 𝑥 ∈ 𝐴 ∧ ( 𝐹 ‘ 𝑥 ) = 0 ) ) )
20	2 19	syl	⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐹 : 𝐴 ⟶ ℂ ∧ 𝐺 : 𝐴 ⟶ ℂ ) → ( 𝑥 ∈ ( ◡ 𝐹 “ { 0 } ) ↔ ( 𝑥 ∈ 𝐴 ∧ ( 𝐹 ‘ 𝑥 ) = 0 ) ) )
21		fniniseg	⊢ ( 𝐺 Fn 𝐴 → ( 𝑥 ∈ ( ◡ 𝐺 “ { 0 } ) ↔ ( 𝑥 ∈ 𝐴 ∧ ( 𝐺 ‘ 𝑥 ) = 0 ) ) )
22	4 21	syl	⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐹 : 𝐴 ⟶ ℂ ∧ 𝐺 : 𝐴 ⟶ ℂ ) → ( 𝑥 ∈ ( ◡ 𝐺 “ { 0 } ) ↔ ( 𝑥 ∈ 𝐴 ∧ ( 𝐺 ‘ 𝑥 ) = 0 ) ) )
23	20 22	orbi12d	⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐹 : 𝐴 ⟶ ℂ ∧ 𝐺 : 𝐴 ⟶ ℂ ) → ( ( 𝑥 ∈ ( ◡ 𝐹 “ { 0 } ) ∨ 𝑥 ∈ ( ◡ 𝐺 “ { 0 } ) ) ↔ ( ( 𝑥 ∈ 𝐴 ∧ ( 𝐹 ‘ 𝑥 ) = 0 ) ∨ ( 𝑥 ∈ 𝐴 ∧ ( 𝐺 ‘ 𝑥 ) = 0 ) ) ) )
24		elun	⊢ ( 𝑥 ∈ ( ( ◡ 𝐹 “ { 0 } ) ∪ ( ◡ 𝐺 “ { 0 } ) ) ↔ ( 𝑥 ∈ ( ◡ 𝐹 “ { 0 } ) ∨ 𝑥 ∈ ( ◡ 𝐺 “ { 0 } ) ) )
25		andi	⊢ ( ( 𝑥 ∈ 𝐴 ∧ ( ( 𝐹 ‘ 𝑥 ) = 0 ∨ ( 𝐺 ‘ 𝑥 ) = 0 ) ) ↔ ( ( 𝑥 ∈ 𝐴 ∧ ( 𝐹 ‘ 𝑥 ) = 0 ) ∨ ( 𝑥 ∈ 𝐴 ∧ ( 𝐺 ‘ 𝑥 ) = 0 ) ) )
26	23 24 25	3bitr4g	⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐹 : 𝐴 ⟶ ℂ ∧ 𝐺 : 𝐴 ⟶ ℂ ) → ( 𝑥 ∈ ( ( ◡ 𝐹 “ { 0 } ) ∪ ( ◡ 𝐺 “ { 0 } ) ) ↔ ( 𝑥 ∈ 𝐴 ∧ ( ( 𝐹 ‘ 𝑥 ) = 0 ∨ ( 𝐺 ‘ 𝑥 ) = 0 ) ) ) )
27	15 18 26	3bitr4d	⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐹 : 𝐴 ⟶ ℂ ∧ 𝐺 : 𝐴 ⟶ ℂ ) → ( 𝑥 ∈ ( ◡ ( 𝐹 ∘f · 𝐺 ) “ { 0 } ) ↔ 𝑥 ∈ ( ( ◡ 𝐹 “ { 0 } ) ∪ ( ◡ 𝐺 “ { 0 } ) ) ) )
28	27	eqrdv	⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐹 : 𝐴 ⟶ ℂ ∧ 𝐺 : 𝐴 ⟶ ℂ ) → ( ◡ ( 𝐹 ∘f · 𝐺 ) “ { 0 } ) = ( ( ◡ 𝐹 “ { 0 } ) ∪ ( ◡ 𝐺 “ { 0 } ) ) )