pjfval

Description: The value of the projection function. (Contributed by Mario Carneiro, 16-Oct-2015)

	Ref	Expression
Hypotheses	pjfval.v	$⊢ V = {Base}_{W}$
	pjfval.l	$⊢ L = LSubSp (W)$
	pjfval.o	$⊢ \underset{˙}{⊥} = ocv (W)$
	pjfval.p	$⊢ P = {proj}_{1} (W)$
	pjfval.k	$⊢ K = proj (W)$
Assertion	pjfval	$⊢ K = (x \in L ⟼ x P \underset{˙}{⊥} (x)) \cap (V \times (V^{V}))$

Proof

Step	Hyp	Ref	Expression
1		pjfval.v	$⊢ V = {Base}_{W}$
2		pjfval.l	$⊢ L = LSubSp (W)$
3		pjfval.o	$⊢ \underset{˙}{⊥} = ocv (W)$
4		pjfval.p	$⊢ P = {proj}_{1} (W)$
5		pjfval.k	$⊢ K = proj (W)$
6		fveq2	$⊢ w = W \to LSubSp (w) = LSubSp (W)$
7	6 2	eqtr4di	$⊢ w = W \to LSubSp (w) = L$
8		fveq2	$⊢ w = W \to {proj}_{1} (w) = {proj}_{1} (W)$
9	8 4	eqtr4di	$⊢ w = W \to {proj}_{1} (w) = P$
10		eqidd	$⊢ w = W \to x = x$
11		fveq2	$⊢ w = W \to ocv (w) = ocv (W)$
12	11 3	eqtr4di	$⊢ w = W \to ocv (w) = \underset{˙}{⊥}$
13	12	fveq1d	$⊢ w = W \to ocv (w) (x) = \underset{˙}{⊥} (x)$
14	9 10 13	oveq123d	$⊢ w = W \to x {proj}_{1} (w) ocv (w) (x) = x P \underset{˙}{⊥} (x)$
15	7 14	mpteq12dv	$⊢ w = W \to (x \in LSubSp (w) ⟼ x {proj}_{1} (w) ocv (w) (x)) = (x \in L ⟼ x P \underset{˙}{⊥} (x))$
16		fveq2	$⊢ w = W \to {Base}_{w} = {Base}_{W}$
17	16 1	eqtr4di	$⊢ w = W \to {Base}_{w} = V$
18	17 17	oveq12d	$⊢ w = W \to {Base}_{w}^{{Base}_{w}} = V^{V}$
19	18	xpeq2d	$⊢ w = W \to V \times ({Base}_{w}^{{Base}_{w}}) = V \times (V^{V})$
20	15 19	ineq12d	$⊢ w = W \to (x \in LSubSp (w) ⟼ x {proj}_{1} (w) ocv (w) (x)) \cap (V \times ({Base}_{w}^{{Base}_{w}})) = (x \in L ⟼ x P \underset{˙}{⊥} (x)) \cap (V \times (V^{V}))$
21		df-pj	$⊢ proj = (w \in V ⟼ (x \in LSubSp (w) ⟼ x {proj}_{1} (w) ocv (w) (x)) \cap (V \times ({Base}_{w}^{{Base}_{w}})))$
22	2	fvexi	$⊢ L \in V$
23	22	inex1	$⊢ L \cap V \in V$
24		ovex	$⊢ V^{V} \in V$
25	24	inex2	$⊢ V \cap (V^{V}) \in V$
26	23 25	xpex	$⊢ (L \cap V) \times (V \cap (V^{V})) \in V$
27		eqid	$⊢ (x \in L ⟼ x P \underset{˙}{⊥} (x)) = (x \in L ⟼ x P \underset{˙}{⊥} (x))$
28		ovexd	$⊢ x \in L \to x P \underset{˙}{⊥} (x) \in V$
29	27 28	fmpti	$⊢ (x \in L ⟼ x P \underset{˙}{⊥} (x)) : L ⟶ V$
30		fssxp	$⊢ (x \in L ⟼ x P \underset{˙}{⊥} (x)) : L ⟶ V \to (x \in L ⟼ x P \underset{˙}{⊥} (x)) \subseteq L \times V$
31		ssrin	$⊢ (x \in L ⟼ x P \underset{˙}{⊥} (x)) \subseteq L \times V \to (x \in L ⟼ x P \underset{˙}{⊥} (x)) \cap (V \times (V^{V})) \subseteq (L \times V) \cap (V \times (V^{V}))$
32	29 30 31	mp2b	$⊢ (x \in L ⟼ x P \underset{˙}{⊥} (x)) \cap (V \times (V^{V})) \subseteq (L \times V) \cap (V \times (V^{V}))$
33		inxp	$⊢ (L \times V) \cap (V \times (V^{V})) = (L \cap V) \times (V \cap (V^{V}))$
34	32 33	sseqtri	$⊢ (x \in L ⟼ x P \underset{˙}{⊥} (x)) \cap (V \times (V^{V})) \subseteq (L \cap V) \times (V \cap (V^{V}))$
35	26 34	ssexi	$⊢ (x \in L ⟼ x P \underset{˙}{⊥} (x)) \cap (V \times (V^{V})) \in V$
36	20 21 35	fvmpt	$⊢ W \in V \to proj (W) = (x \in L ⟼ x P \underset{˙}{⊥} (x)) \cap (V \times (V^{V}))$
37		fvprc	$⊢ \neg W \in V \to proj (W) = \emptyset$
38		inss1	$⊢ (x \in L ⟼ x P \underset{˙}{⊥} (x)) \cap (V \times (V^{V})) \subseteq (x \in L ⟼ x P \underset{˙}{⊥} (x))$
39		fvprc	$⊢ \neg W \in V \to LSubSp (W) = \emptyset$
40	2 39	syl5eq	$⊢ \neg W \in V \to L = \emptyset$
41	40	mpteq1d	$⊢ \neg W \in V \to (x \in L ⟼ x P \underset{˙}{⊥} (x)) = (x \in \emptyset ⟼ x P \underset{˙}{⊥} (x))$
42		mpt0	$⊢ (x \in \emptyset ⟼ x P \underset{˙}{⊥} (x)) = \emptyset$
43	41 42	eqtrdi	$⊢ \neg W \in V \to (x \in L ⟼ x P \underset{˙}{⊥} (x)) = \emptyset$
44		sseq0	$⊢ ((x \in L ⟼ x P \underset{˙}{⊥} (x)) \cap (V \times (V^{V})) \subseteq (x \in L ⟼ x P \underset{˙}{⊥} (x)) \land (x \in L ⟼ x P \underset{˙}{⊥} (x)) = \emptyset) \to (x \in L ⟼ x P \underset{˙}{⊥} (x)) \cap (V \times (V^{V})) = \emptyset$
45	38 43 44	sylancr	$⊢ \neg W \in V \to (x \in L ⟼ x P \underset{˙}{⊥} (x)) \cap (V \times (V^{V})) = \emptyset$
46	37 45	eqtr4d	$⊢ \neg W \in V \to proj (W) = (x \in L ⟼ x P \underset{˙}{⊥} (x)) \cap (V \times (V^{V}))$
47	36 46	pm2.61i	$⊢ proj (W) = (x \in L ⟼ x P \underset{˙}{⊥} (x)) \cap (V \times (V^{V}))$
48	5 47	eqtri	$⊢ K = (x \in L ⟼ x P \underset{˙}{⊥} (x)) \cap (V \times (V^{V}))$

Metamath Proof Explorer

Theorem pjfval

Proof