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 \in V \land F : A ⟶ ℂ \land G : A ⟶ ℂ) \to {(F \times_{f} G)}^{-1} [\{0\}] = F^{-1} [\{0\}] \cup G^{-1} [\{0\}]$

Proof

Step	Hyp	Ref	Expression
1		simp2	$⊢ (A \in V \land F : A ⟶ ℂ \land G : A ⟶ ℂ) \to F : A ⟶ ℂ$
2	1	ffnd	$⊢ (A \in V \land F : A ⟶ ℂ \land G : A ⟶ ℂ) \to F Fn A$
3		simp3	$⊢ (A \in V \land F : A ⟶ ℂ \land G : A ⟶ ℂ) \to G : A ⟶ ℂ$
4	3	ffnd	$⊢ (A \in V \land F : A ⟶ ℂ \land G : A ⟶ ℂ) \to G Fn A$
5		simp1	$⊢ (A \in V \land F : A ⟶ ℂ \land G : A ⟶ ℂ) \to A \in V$
6		inidm	$⊢ A \cap A = A$
7		eqidd	$⊢ ((A \in V \land F : A ⟶ ℂ \land G : A ⟶ ℂ) \land x \in A) \to F (x) = F (x)$
8		eqidd	$⊢ ((A \in V \land F : A ⟶ ℂ \land G : A ⟶ ℂ) \land x \in A) \to G (x) = G (x)$
9	2 4 5 5 6 7 8	ofval	$⊢ ((A \in V \land F : A ⟶ ℂ \land G : A ⟶ ℂ) \land x \in A) \to (F \times_{f} G) (x) = F (x) G (x)$
10	9	eqeq1d	$⊢ ((A \in V \land F : A ⟶ ℂ \land G : A ⟶ ℂ) \land x \in A) \to ((F \times_{f} G) (x) = 0 \leftrightarrow F (x) G (x) = 0)$
11	1	ffvelrnda	$⊢ ((A \in V \land F : A ⟶ ℂ \land G : A ⟶ ℂ) \land x \in A) \to F (x) \in ℂ$
12	3	ffvelrnda	$⊢ ((A \in V \land F : A ⟶ ℂ \land G : A ⟶ ℂ) \land x \in A) \to G (x) \in ℂ$
13	11 12	mul0ord	$⊢ ((A \in V \land F : A ⟶ ℂ \land G : A ⟶ ℂ) \land x \in A) \to (F (x) G (x) = 0 \leftrightarrow (F (x) = 0 \lor G (x) = 0))$
14	10 13	bitrd	$⊢ ((A \in V \land F : A ⟶ ℂ \land G : A ⟶ ℂ) \land x \in A) \to ((F \times_{f} G) (x) = 0 \leftrightarrow (F (x) = 0 \lor G (x) = 0))$
15	14	pm5.32da	$⊢ (A \in V \land F : A ⟶ ℂ \land G : A ⟶ ℂ) \to ((x \in A \land (F \times_{f} G) (x) = 0) \leftrightarrow (x \in A \land (F (x) = 0 \lor G (x) = 0)))$
16	2 4 5 5 6	offn	$⊢ (A \in V \land F : A ⟶ ℂ \land G : A ⟶ ℂ) \to (F \times_{f} G) Fn A$
17		fniniseg	$⊢ (F \times_{f} G) Fn A \to (x \in {(F \times_{f} G)}^{-1} [\{0\}] \leftrightarrow (x \in A \land (F \times_{f} G) (x) = 0))$
18	16 17	syl	$⊢ (A \in V \land F : A ⟶ ℂ \land G : A ⟶ ℂ) \to (x \in {(F \times_{f} G)}^{-1} [\{0\}] \leftrightarrow (x \in A \land (F \times_{f} G) (x) = 0))$
19		fniniseg	$⊢ F Fn A \to (x \in F^{-1} [\{0\}] \leftrightarrow (x \in A \land F (x) = 0))$
20	2 19	syl	$⊢ (A \in V \land F : A ⟶ ℂ \land G : A ⟶ ℂ) \to (x \in F^{-1} [\{0\}] \leftrightarrow (x \in A \land F (x) = 0))$
21		fniniseg	$⊢ G Fn A \to (x \in G^{-1} [\{0\}] \leftrightarrow (x \in A \land G (x) = 0))$
22	4 21	syl	$⊢ (A \in V \land F : A ⟶ ℂ \land G : A ⟶ ℂ) \to (x \in G^{-1} [\{0\}] \leftrightarrow (x \in A \land G (x) = 0))$
23	20 22	orbi12d	$⊢ (A \in V \land F : A ⟶ ℂ \land G : A ⟶ ℂ) \to ((x \in F^{-1} [\{0\}] \lor x \in G^{-1} [\{0\}]) \leftrightarrow ((x \in A \land F (x) = 0) \lor (x \in A \land G (x) = 0)))$
24		elun	$⊢ x \in (F^{-1} [\{0\}] \cup G^{-1} [\{0\}]) \leftrightarrow (x \in F^{-1} [\{0\}] \lor x \in G^{-1} [\{0\}])$
25		andi	$⊢ (x \in A \land (F (x) = 0 \lor G (x) = 0)) \leftrightarrow ((x \in A \land F (x) = 0) \lor (x \in A \land G (x) = 0))$
26	23 24 25	3bitr4g	$⊢ (A \in V \land F : A ⟶ ℂ \land G : A ⟶ ℂ) \to (x \in (F^{-1} [\{0\}] \cup G^{-1} [\{0\}]) \leftrightarrow (x \in A \land (F (x) = 0 \lor G (x) = 0)))$
27	15 18 26	3bitr4d	$⊢ (A \in V \land F : A ⟶ ℂ \land G : A ⟶ ℂ) \to (x \in {(F \times_{f} G)}^{-1} [\{0\}] \leftrightarrow x \in (F^{-1} [\{0\}] \cup G^{-1} [\{0\}]))$
28	27	eqrdv	$⊢ (A \in V \land F : A ⟶ ℂ \land G : A ⟶ ℂ) \to {(F \times_{f} G)}^{-1} [\{0\}] = F^{-1} [\{0\}] \cup G^{-1} [\{0\}]$

Metamath Proof Explorer

Theorem ofmulrt

Proof