prjspnval2

Description: Value of the n-dimensional projective space function, expanded. (Contributed by Steven Nguyen, 15-Jul-2023)

	Ref	Expression
Hypotheses	prjspnval2.e	$⊢ \underset{˙}{\sim} = \{⟨x, y⟩ \| ((x \in B \land y \in B) \land \exists l \in S x = l \underset{˙}{\cdot} y)\}$
	prjspnval2.w	$⊢ W = K freeLMod (0 \dots N)$
	prjspnval2.b	$⊢ B = {Base}_{W} ∖ \{0_{W}\}$
	prjspnval2.s	$⊢ S = {Base}_{K}$
	prjspnval2.x	$⊢ \underset{˙}{\cdot} = \cdot_{W}$
Assertion	prjspnval2	$⊢ (N \in ℕ_{0} \land K \in DivRing) \to N {ℙ𝕣𝕠𝕛}_{n} K = B / \underset{˙}{\sim}$

Proof

Step	Hyp	Ref	Expression
1		prjspnval2.e	$⊢ \underset{˙}{\sim} = \{⟨x, y⟩ \| ((x \in B \land y \in B) \land \exists l \in S x = l \underset{˙}{\cdot} y)\}$
2		prjspnval2.w	$⊢ W = K freeLMod (0 \dots N)$
3		prjspnval2.b	$⊢ B = {Base}_{W} ∖ \{0_{W}\}$
4		prjspnval2.s	$⊢ S = {Base}_{K}$
5		prjspnval2.x	$⊢ \underset{˙}{\cdot} = \cdot_{W}$
6		prjspnval	$⊢ (N \in ℕ_{0} \land K \in DivRing) \to N {ℙ𝕣𝕠𝕛}_{n} K = ℙ𝕣𝕠𝕛 (K freeLMod (0 \dots N))$
7		simpr	$⊢ (N \in ℕ_{0} \land K \in DivRing) \to K \in DivRing$
8		ovexd	$⊢ (N \in ℕ_{0} \land K \in DivRing) \to (0 \dots N) \in V$
9	2	frlmlvec	$⊢ (K \in DivRing \land (0 \dots N) \in V) \to W \in LVec$
10	7 8 9	syl2anc	$⊢ (N \in ℕ_{0} \land K \in DivRing) \to W \in LVec$
11		eqid	$⊢ Scalar (W) = Scalar (W)$
12		eqid	$⊢ {Base}_{Scalar (W)} = {Base}_{Scalar (W)}$
13	3 5 11 12	prjspval	$⊢ W \in LVec \to ℙ𝕣𝕠𝕛 (W) = B / \{⟨x, y⟩ \| ((x \in B \land y \in B) \land \exists l \in {Base}_{Scalar (W)} x = l \underset{˙}{\cdot} y)\}$
14	10 13	syl	$⊢ (N \in ℕ_{0} \land K \in DivRing) \to ℙ𝕣𝕠𝕛 (W) = B / \{⟨x, y⟩ \| ((x \in B \land y \in B) \land \exists l \in {Base}_{Scalar (W)} x = l \underset{˙}{\cdot} y)\}$
15	2	frlmsca	$⊢ (K \in DivRing \land (0 \dots N) \in V) \to K = Scalar (W)$
16	7 8 15	syl2anc	$⊢ (N \in ℕ_{0} \land K \in DivRing) \to K = Scalar (W)$
17	16	fveq2d	$⊢ (N \in ℕ_{0} \land K \in DivRing) \to {Base}_{K} = {Base}_{Scalar (W)}$
18	4 17	syl5req	$⊢ (N \in ℕ_{0} \land K \in DivRing) \to {Base}_{Scalar (W)} = S$
19	18	rexeqdv	$⊢ (N \in ℕ_{0} \land K \in DivRing) \to (\exists l \in {Base}_{Scalar (W)} x = l \underset{˙}{\cdot} y \leftrightarrow \exists l \in S x = l \underset{˙}{\cdot} y)$
20	19	anbi2d	$⊢ (N \in ℕ_{0} \land K \in DivRing) \to (((x \in B \land y \in B) \land \exists l \in {Base}_{Scalar (W)} x = l \underset{˙}{\cdot} y) \leftrightarrow ((x \in B \land y \in B) \land \exists l \in S x = l \underset{˙}{\cdot} y))$
21	20	opabbidv	$⊢ (N \in ℕ_{0} \land K \in DivRing) \to \{⟨x, y⟩ \| ((x \in B \land y \in B) \land \exists l \in {Base}_{Scalar (W)} x = l \underset{˙}{\cdot} y)\} = \{⟨x, y⟩ \| ((x \in B \land y \in B) \land \exists l \in S x = l \underset{˙}{\cdot} y)\}$
22	21	qseq2d	$⊢ (N \in ℕ_{0} \land K \in DivRing) \to B / \{⟨x, y⟩ \| ((x \in B \land y \in B) \land \exists l \in {Base}_{Scalar (W)} x = l \underset{˙}{\cdot} y)\} = B / \{⟨x, y⟩ \| ((x \in B \land y \in B) \land \exists l \in S x = l \underset{˙}{\cdot} y)\}$
23	14 22	eqtrd	$⊢ (N \in ℕ_{0} \land K \in DivRing) \to ℙ𝕣𝕠𝕛 (W) = B / \{⟨x, y⟩ \| ((x \in B \land y \in B) \land \exists l \in S x = l \underset{˙}{\cdot} y)\}$
24	2	eqcomi	$⊢ K freeLMod (0 \dots N) = W$
25	24	fveq2i	$⊢ ℙ𝕣𝕠𝕛 (K freeLMod (0 \dots N)) = ℙ𝕣𝕠𝕛 (W)$
26	1	qseq2i	$⊢ B / \underset{˙}{\sim} = B / \{⟨x, y⟩ \| ((x \in B \land y \in B) \land \exists l \in S x = l \underset{˙}{\cdot} y)\}$
27	23 25 26	3eqtr4g	$⊢ (N \in ℕ_{0} \land K \in DivRing) \to ℙ𝕣𝕠𝕛 (K freeLMod (0 \dots N)) = B / \underset{˙}{\sim}$
28	6 27	eqtrd	$⊢ (N \in ℕ_{0} \land K \in DivRing) \to N {ℙ𝕣𝕠𝕛}_{n} K = B / \underset{˙}{\sim}$

Metamath Proof Explorer

Theorem prjspnval2

Proof