pjfval2

Description: Value of the projection map with implicit domain. (Contributed by Mario Carneiro, 16-Oct-2015)

	Ref	Expression
Hypotheses	pjfval2.o	$⊢ \underset{˙}{⊥} = ocv (W)$
	pjfval2.p	$⊢ P = {proj}_{1} (W)$
	pjfval2.k	$⊢ K = proj (W)$
Assertion	pjfval2	$⊢ K = (x \in dom K ⟼ x P \underset{˙}{⊥} (x))$

Proof

Step	Hyp	Ref	Expression
1		pjfval2.o	$⊢ \underset{˙}{⊥} = ocv (W)$
2		pjfval2.p	$⊢ P = {proj}_{1} (W)$
3		pjfval2.k	$⊢ K = proj (W)$
4		df-mpt	$⊢ (x \in LSubSp (W) ⟼ x P \underset{˙}{⊥} (x)) = \{⟨x, y⟩ \| (x \in LSubSp (W) \land y = x P \underset{˙}{⊥} (x))\}$
5		df-xp	$⊢ V \times ({Base}_{W}^{{Base}_{W}}) = \{⟨x, y⟩ \| (x \in V \land y \in ({Base}_{W}^{{Base}_{W}}))\}$
6	4 5	ineq12i	$⊢ (x \in LSubSp (W) ⟼ x P \underset{˙}{⊥} (x)) \cap (V \times ({Base}_{W}^{{Base}_{W}})) = \{⟨x, y⟩ \| (x \in LSubSp (W) \land y = x P \underset{˙}{⊥} (x))\} \cap \{⟨x, y⟩ \| (x \in V \land y \in ({Base}_{W}^{{Base}_{W}}))\}$
7		eqid	$⊢ {Base}_{W} = {Base}_{W}$
8		eqid	$⊢ LSubSp (W) = LSubSp (W)$
9	7 8 1 2 3	pjfval	$⊢ K = (x \in LSubSp (W) ⟼ x P \underset{˙}{⊥} (x)) \cap (V \times ({Base}_{W}^{{Base}_{W}}))$
10	7 8 1 2 3	pjdm	$⊢ x \in dom K \leftrightarrow (x \in LSubSp (W) \land (x P \underset{˙}{⊥} (x)) : {Base}_{W} ⟶ {Base}_{W})$
11		eleq1	$⊢ y = x P \underset{˙}{⊥} (x) \to (y \in ({Base}_{W}^{{Base}_{W}}) \leftrightarrow x P \underset{˙}{⊥} (x) \in ({Base}_{W}^{{Base}_{W}}))$
12		fvex	$⊢ {Base}_{W} \in V$
13	12 12	elmap	$⊢ x P \underset{˙}{⊥} (x) \in ({Base}_{W}^{{Base}_{W}}) \leftrightarrow (x P \underset{˙}{⊥} (x)) : {Base}_{W} ⟶ {Base}_{W}$
14	11 13	bitr2di	$⊢ y = x P \underset{˙}{⊥} (x) \to ((x P \underset{˙}{⊥} (x)) : {Base}_{W} ⟶ {Base}_{W} \leftrightarrow y \in ({Base}_{W}^{{Base}_{W}}))$
15	14	anbi2d	$⊢ y = x P \underset{˙}{⊥} (x) \to ((x \in LSubSp (W) \land (x P \underset{˙}{⊥} (x)) : {Base}_{W} ⟶ {Base}_{W}) \leftrightarrow (x \in LSubSp (W) \land y \in ({Base}_{W}^{{Base}_{W}})))$
16	10 15	syl5bb	$⊢ y = x P \underset{˙}{⊥} (x) \to (x \in dom K \leftrightarrow (x \in LSubSp (W) \land y \in ({Base}_{W}^{{Base}_{W}})))$
17	16	pm5.32ri	$⊢ (x \in dom K \land y = x P \underset{˙}{⊥} (x)) \leftrightarrow ((x \in LSubSp (W) \land y \in ({Base}_{W}^{{Base}_{W}})) \land y = x P \underset{˙}{⊥} (x))$
18		an32	$⊢ ((x \in LSubSp (W) \land y \in ({Base}_{W}^{{Base}_{W}})) \land y = x P \underset{˙}{⊥} (x)) \leftrightarrow ((x \in LSubSp (W) \land y = x P \underset{˙}{⊥} (x)) \land y \in ({Base}_{W}^{{Base}_{W}}))$
19		vex	$⊢ x \in V$
20	19	biantrur	$⊢ y \in ({Base}_{W}^{{Base}_{W}}) \leftrightarrow (x \in V \land y \in ({Base}_{W}^{{Base}_{W}}))$
21	20	anbi2i	$⊢ ((x \in LSubSp (W) \land y = x P \underset{˙}{⊥} (x)) \land y \in ({Base}_{W}^{{Base}_{W}})) \leftrightarrow ((x \in LSubSp (W) \land y = x P \underset{˙}{⊥} (x)) \land (x \in V \land y \in ({Base}_{W}^{{Base}_{W}})))$
22	17 18 21	3bitri	$⊢ (x \in dom K \land y = x P \underset{˙}{⊥} (x)) \leftrightarrow ((x \in LSubSp (W) \land y = x P \underset{˙}{⊥} (x)) \land (x \in V \land y \in ({Base}_{W}^{{Base}_{W}})))$
23	22	opabbii	$⊢ \{⟨x, y⟩ \| (x \in dom K \land y = x P \underset{˙}{⊥} (x))\} = \{⟨x, y⟩ \| ((x \in LSubSp (W) \land y = x P \underset{˙}{⊥} (x)) \land (x \in V \land y \in ({Base}_{W}^{{Base}_{W}})))\}$
24		df-mpt	$⊢ (x \in dom K ⟼ x P \underset{˙}{⊥} (x)) = \{⟨x, y⟩ \| (x \in dom K \land y = x P \underset{˙}{⊥} (x))\}$
25		inopab	$⊢ \{⟨x, y⟩ \| (x \in LSubSp (W) \land y = x P \underset{˙}{⊥} (x))\} \cap \{⟨x, y⟩ \| (x \in V \land y \in ({Base}_{W}^{{Base}_{W}}))\} = \{⟨x, y⟩ \| ((x \in LSubSp (W) \land y = x P \underset{˙}{⊥} (x)) \land (x \in V \land y \in ({Base}_{W}^{{Base}_{W}})))\}$
26	23 24 25	3eqtr4i	$⊢ (x \in dom K ⟼ x P \underset{˙}{⊥} (x)) = \{⟨x, y⟩ \| (x \in LSubSp (W) \land y = x P \underset{˙}{⊥} (x))\} \cap \{⟨x, y⟩ \| (x \in V \land y \in ({Base}_{W}^{{Base}_{W}}))\}$
27	6 9 26	3eqtr4i	$⊢ K = (x \in dom K ⟼ x P \underset{˙}{⊥} (x))$

Metamath Proof Explorer

Theorem pjfval2

Proof