Metamath Proof Explorer

Theorem pjdm

Description: A subspace is in the domain of the projection function iff the subspace admits a projection decomposition of the whole space. (Contributed by Mario Carneiro, 16-Oct-2015)

Ref Expression
Hypotheses pjfval.v ⊢ V = Base W
pjfval.l ⊢ L = LSubSp ⁡ W
pjfval.o ⊢ ⊥ ˙ = ocv ⁡ W
pjfval.p ⊢ P = proj 1 ⁡ W
pjfval.k ⊢ K = proj ⁡ W
Assertion pjdm ⊢ T ∈ dom ⁡ K ↔ T ∈ L ∧ T P ⊥ ˙ ⁡ T : V ⟶ V

Proof

Step Hyp Ref Expression
1 pjfval.v ⊢ V = Base W
2 pjfval.l ⊢ L = LSubSp ⁡ W
3 pjfval.o ⊢ ⊥ ˙ = ocv ⁡ W
4 pjfval.p ⊢ P = proj 1 ⁡ W
5 pjfval.k ⊢ K = proj ⁡ W
6 id ⊢ x = T → x = T
7 fveq2 ⊢ x = T → ⊥ ˙ ⁡ x = ⊥ ˙ ⁡ T
8 6 7 oveq12d ⊢ x = T → x P ⊥ ˙ ⁡ x = T P ⊥ ˙ ⁡ T
9 8 eleq1d ⊢ x = T → x P ⊥ ˙ ⁡ x ∈ V V ↔ T P ⊥ ˙ ⁡ T ∈ V V
10 1 fvexi ⊢ V ∈ V
11 10 10 elmap ⊢ T P ⊥ ˙ ⁡ T ∈ V V ↔ T P ⊥ ˙ ⁡ T : V ⟶ V
12 9 11 bitrdi ⊢ x = T → x P ⊥ ˙ ⁡ x ∈ V V ↔ T P ⊥ ˙ ⁡ T : V ⟶ V
13 cnvin ⊢ x ∈ L ⟼ x P ⊥ ˙ ⁡ x ∩ V × V V -1 = x ∈ L ⟼ x P ⊥ ˙ ⁡ x -1 ∩ V × V V -1
14 cnvxp ⊢ V × V V -1 = V V × V
15 14 ineq2i ⊢ x ∈ L ⟼ x P ⊥ ˙ ⁡ x -1 ∩ V × V V -1 = x ∈ L ⟼ x P ⊥ ˙ ⁡ x -1 ∩ V V × V
16 13 15 eqtri ⊢ x ∈ L ⟼ x P ⊥ ˙ ⁡ x ∩ V × V V -1 = x ∈ L ⟼ x P ⊥ ˙ ⁡ x -1 ∩ V V × V
17 1 2 3 4 5 pjfval ⊢ K = x ∈ L ⟼ x P ⊥ ˙ ⁡ x ∩ V × V V
18 17 cnveqi ⊢ K -1 = x ∈ L ⟼ x P ⊥ ˙ ⁡ x ∩ V × V V -1
19 df-res ⊢ x ∈ L ⟼ x P ⊥ ˙ ⁡ x -1 ↾ V V = x ∈ L ⟼ x P ⊥ ˙ ⁡ x -1 ∩ V V × V
20 16 18 19 3eqtr4i ⊢ K -1 = x ∈ L ⟼ x P ⊥ ˙ ⁡ x -1 ↾ V V
21 20 rneqi ⊢ ran ⁡ K -1 = ran ⁡ x ∈ L ⟼ x P ⊥ ˙ ⁡ x -1 ↾ V V
22 dfdm4 ⊢ dom ⁡ K = ran ⁡ K -1
23 df-ima ⊢ x ∈ L ⟼ x P ⊥ ˙ ⁡ x -1 V V = ran ⁡ x ∈ L ⟼ x P ⊥ ˙ ⁡ x -1 ↾ V V
24 21 22 23 3eqtr4i ⊢ dom ⁡ K = x ∈ L ⟼ x P ⊥ ˙ ⁡ x -1 V V
25 eqid ⊢ x ∈ L ⟼ x P ⊥ ˙ ⁡ x = x ∈ L ⟼ x P ⊥ ˙ ⁡ x
26 25 mptpreima ⊢ x ∈ L ⟼ x P ⊥ ˙ ⁡ x -1 V V = x ∈ L | x P ⊥ ˙ ⁡ x ∈ V V
27 24 26 eqtri ⊢ dom ⁡ K = x ∈ L | x P ⊥ ˙ ⁡ x ∈ V V
28 12 27 elrab2 ⊢ T ∈ dom ⁡ K ↔ T ∈ L ∧ T P ⊥ ˙ ⁡ T : V ⟶ V