Metamath Proof Explorer

Theorem mbfconstlem

Description: Lemma for mbfconst and related theorems. (Contributed by Mario Carneiro, 17-Jun-2014)

Ref Expression
Assertion mbfconstlem ⊢ A ∈ dom ⁡ vol ∧ C ∈ ℝ → A × C -1 B ∈ dom ⁡ vol

Proof

Step Hyp Ref Expression
1 cnvimass ⊢ A × C -1 B ⊆ dom ⁡ A × C
2 1 a1i ⊢ A ∈ dom ⁡ vol ∧ C ∈ ℝ ∧ C ∈ B → A × C -1 B ⊆ dom ⁡ A × C
3 cnvimarndm ⊢ A × C -1 ran ⁡ A × C = dom ⁡ A × C
4 fconst6g ⊢ C ∈ B → A × C : A ⟶ B
5 4 adantl ⊢ A ∈ dom ⁡ vol ∧ C ∈ ℝ ∧ C ∈ B → A × C : A ⟶ B
6 frn ⊢ A × C : A ⟶ B → ran ⁡ A × C ⊆ B
7 imass2 ⊢ ran ⁡ A × C ⊆ B → A × C -1 ran ⁡ A × C ⊆ A × C -1 B
8 5 6 7 3syl ⊢ A ∈ dom ⁡ vol ∧ C ∈ ℝ ∧ C ∈ B → A × C -1 ran ⁡ A × C ⊆ A × C -1 B
9 3 8 eqsstrrid ⊢ A ∈ dom ⁡ vol ∧ C ∈ ℝ ∧ C ∈ B → dom ⁡ A × C ⊆ A × C -1 B
10 2 9 eqssd ⊢ A ∈ dom ⁡ vol ∧ C ∈ ℝ ∧ C ∈ B → A × C -1 B = dom ⁡ A × C
11 fconstg ⊢ C ∈ ℝ → A × C : A ⟶ C
12 11 ad2antlr ⊢ A ∈ dom ⁡ vol ∧ C ∈ ℝ ∧ C ∈ B → A × C : A ⟶ C
13 12 fdmd ⊢ A ∈ dom ⁡ vol ∧ C ∈ ℝ ∧ C ∈ B → dom ⁡ A × C = A
14 10 13 eqtrd ⊢ A ∈ dom ⁡ vol ∧ C ∈ ℝ ∧ C ∈ B → A × C -1 B = A
15 simpll ⊢ A ∈ dom ⁡ vol ∧ C ∈ ℝ ∧ C ∈ B → A ∈ dom ⁡ vol
16 14 15 eqeltrd ⊢ A ∈ dom ⁡ vol ∧ C ∈ ℝ ∧ C ∈ B → A × C -1 B ∈ dom ⁡ vol
17 11 ad2antlr ⊢ A ∈ dom ⁡ vol ∧ C ∈ ℝ ∧ ¬ C ∈ B → A × C : A ⟶ C
18 incom ⊢ C ∩ B = B ∩ C
19 simpr ⊢ A ∈ dom ⁡ vol ∧ C ∈ ℝ ∧ ¬ C ∈ B → ¬ C ∈ B
20 disjsn ⊢ B ∩ C = ∅ ↔ ¬ C ∈ B
21 19 20 sylibr ⊢ A ∈ dom ⁡ vol ∧ C ∈ ℝ ∧ ¬ C ∈ B → B ∩ C = ∅
22 18 21 syl5eq ⊢ A ∈ dom ⁡ vol ∧ C ∈ ℝ ∧ ¬ C ∈ B → C ∩ B = ∅
23 fimacnvdisj ⊢ A × C : A ⟶ C ∧ C ∩ B = ∅ → A × C -1 B = ∅
24 17 22 23 syl2anc ⊢ A ∈ dom ⁡ vol ∧ C ∈ ℝ ∧ ¬ C ∈ B → A × C -1 B = ∅
25 0mbl ⊢ ∅ ∈ dom ⁡ vol
26 24 25 eqeltrdi ⊢ A ∈ dom ⁡ vol ∧ C ∈ ℝ ∧ ¬ C ∈ B → A × C -1 B ∈ dom ⁡ vol
27 16 26 pm2.61dan ⊢ A ∈ dom ⁡ vol ∧ C ∈ ℝ → A × C -1 B ∈ dom ⁡ vol