Metamath Proof Explorer


Theorem pclfvalN

Description: The projective subspace closure function. (Contributed by NM, 7-Sep-2013) (New usage is discouraged.)

Ref Expression
Hypotheses pclfval.a A = Atoms K
pclfval.s S = PSubSp K
pclfval.c U = PCl K
Assertion pclfvalN K V U = x 𝒫 A y S | x y

Proof

Step Hyp Ref Expression
1 pclfval.a A = Atoms K
2 pclfval.s S = PSubSp K
3 pclfval.c U = PCl K
4 elex K V K V
5 fveq2 k = K Atoms k = Atoms K
6 5 1 eqtr4di k = K Atoms k = A
7 6 pweqd k = K 𝒫 Atoms k = 𝒫 A
8 fveq2 k = K PSubSp k = PSubSp K
9 8 2 eqtr4di k = K PSubSp k = S
10 9 rabeqdv k = K y PSubSp k | x y = y S | x y
11 10 inteqd k = K y PSubSp k | x y = y S | x y
12 7 11 mpteq12dv k = K x 𝒫 Atoms k y PSubSp k | x y = x 𝒫 A y S | x y
13 df-pclN PCl = k V x 𝒫 Atoms k y PSubSp k | x y
14 1 fvexi A V
15 14 pwex 𝒫 A V
16 15 mptex x 𝒫 A y S | x y V
17 12 13 16 fvmpt K V PCl K = x 𝒫 A y S | x y
18 3 17 syl5eq K V U = x 𝒫 A y S | x y
19 4 18 syl K V U = x 𝒫 A y S | x y