prjspertr

Description: The relation in PrjSp is transitive. (Contributed by Steven Nguyen, 1-May-2023)

	Ref	Expression
Hypotheses	prjsprel.1	$⊢ \underset{˙}{\sim} = \{⟨x, y⟩ \| ((x \in B \land y \in B) \land \exists l \in K x = l \underset{˙}{\cdot} y)\}$
	prjspertr.b	$⊢ B = {Base}_{V} ∖ \{0_{V}\}$
	prjspertr.s	$⊢ S = Scalar (V)$
	prjspertr.x	$⊢ \underset{˙}{\cdot} = \cdot_{V}$
	prjspertr.k	$⊢ K = {Base}_{S}$
Assertion	prjspertr	$⊢ (V \in LMod \land (X \underset{˙}{\sim} Y \land Y \underset{˙}{\sim} Z)) \to X \underset{˙}{\sim} Z$

Proof

Step	Hyp	Ref	Expression
1		prjsprel.1	$⊢ \underset{˙}{\sim} = \{⟨x, y⟩ \| ((x \in B \land y \in B) \land \exists l \in K x = l \underset{˙}{\cdot} y)\}$
2		prjspertr.b	$⊢ B = {Base}_{V} ∖ \{0_{V}\}$
3		prjspertr.s	$⊢ S = Scalar (V)$
4		prjspertr.x	$⊢ \underset{˙}{\cdot} = \cdot_{V}$
5		prjspertr.k	$⊢ K = {Base}_{S}$
6	1	prjsprel	$⊢ X \underset{˙}{\sim} Y \leftrightarrow ((X \in B \land Y \in B) \land \exists m \in K X = m \underset{˙}{\cdot} Y)$
7	6	simprbi	$⊢ X \underset{˙}{\sim} Y \to \exists m \in K X = m \underset{˙}{\cdot} Y$
8	7	ad2antrl	$⊢ (V \in LMod \land (X \underset{˙}{\sim} Y \land Y \underset{˙}{\sim} Z)) \to \exists m \in K X = m \underset{˙}{\cdot} Y$
9		simplrr	$⊢ ((V \in LMod \land (X \underset{˙}{\sim} Y \land Y \underset{˙}{\sim} Z)) \land (m \in K \land X = m \underset{˙}{\cdot} Y)) \to Y \underset{˙}{\sim} Z$
10	1	prjsprel	$⊢ Y \underset{˙}{\sim} Z \leftrightarrow ((Y \in B \land Z \in B) \land \exists n \in K Y = n \underset{˙}{\cdot} Z)$
11	10	simprbi	$⊢ Y \underset{˙}{\sim} Z \to \exists n \in K Y = n \underset{˙}{\cdot} Z$
12	9 11	syl	$⊢ ((V \in LMod \land (X \underset{˙}{\sim} Y \land Y \underset{˙}{\sim} Z)) \land (m \in K \land X = m \underset{˙}{\cdot} Y)) \to \exists n \in K Y = n \underset{˙}{\cdot} Z$
13		simplrl	$⊢ ((V \in LMod \land (X \underset{˙}{\sim} Y \land Y \underset{˙}{\sim} Z)) \land ((m \in K \land X = m \underset{˙}{\cdot} Y) \land (n \in K \land Y = n \underset{˙}{\cdot} Z))) \to X \underset{˙}{\sim} Y$
14	13	anassrs	$⊢ (((V \in LMod \land (X \underset{˙}{\sim} Y \land Y \underset{˙}{\sim} Z)) \land (m \in K \land X = m \underset{˙}{\cdot} Y)) \land (n \in K \land Y = n \underset{˙}{\cdot} Z)) \to X \underset{˙}{\sim} Y$
15		simpll	$⊢ ((X \in B \land Y \in B) \land \exists m \in K X = m \underset{˙}{\cdot} Y) \to X \in B$
16	6 15	sylbi	$⊢ X \underset{˙}{\sim} Y \to X \in B$
17	14 16	syl	$⊢ (((V \in LMod \land (X \underset{˙}{\sim} Y \land Y \underset{˙}{\sim} Z)) \land (m \in K \land X = m \underset{˙}{\cdot} Y)) \land (n \in K \land Y = n \underset{˙}{\cdot} Z)) \to X \in B$
18	9	adantr	$⊢ (((V \in LMod \land (X \underset{˙}{\sim} Y \land Y \underset{˙}{\sim} Z)) \land (m \in K \land X = m \underset{˙}{\cdot} Y)) \land (n \in K \land Y = n \underset{˙}{\cdot} Z)) \to Y \underset{˙}{\sim} Z$
19		simplr	$⊢ ((Y \in B \land Z \in B) \land \exists n \in K Y = n \underset{˙}{\cdot} Z) \to Z \in B$
20	10 19	sylbi	$⊢ Y \underset{˙}{\sim} Z \to Z \in B$
21	18 20	syl	$⊢ (((V \in LMod \land (X \underset{˙}{\sim} Y \land Y \underset{˙}{\sim} Z)) \land (m \in K \land X = m \underset{˙}{\cdot} Y)) \land (n \in K \land Y = n \underset{˙}{\cdot} Z)) \to Z \in B$
22	3	lmodring	$⊢ V \in LMod \to S \in Ring$
23	22	ad3antrrr	$⊢ (((V \in LMod \land (X \underset{˙}{\sim} Y \land Y \underset{˙}{\sim} Z)) \land (m \in K \land X = m \underset{˙}{\cdot} Y)) \land (n \in K \land Y = n \underset{˙}{\cdot} Z)) \to S \in Ring$
24		simplrl	$⊢ (((V \in LMod \land (X \underset{˙}{\sim} Y \land Y \underset{˙}{\sim} Z)) \land (m \in K \land X = m \underset{˙}{\cdot} Y)) \land (n \in K \land Y = n \underset{˙}{\cdot} Z)) \to m \in K$
25		simprl	$⊢ (((V \in LMod \land (X \underset{˙}{\sim} Y \land Y \underset{˙}{\sim} Z)) \land (m \in K \land X = m \underset{˙}{\cdot} Y)) \land (n \in K \land Y = n \underset{˙}{\cdot} Z)) \to n \in K$
26		eqid	$⊢ \cdot_{S} = \cdot_{S}$
27	5 26	ringcl	$⊢ (S \in Ring \land m \in K \land n \in K) \to m \cdot_{S} n \in K$
28	23 24 25 27	syl3anc	$⊢ (((V \in LMod \land (X \underset{˙}{\sim} Y \land Y \underset{˙}{\sim} Z)) \land (m \in K \land X = m \underset{˙}{\cdot} Y)) \land (n \in K \land Y = n \underset{˙}{\cdot} Z)) \to m \cdot_{S} n \in K$
29		oveq1	$⊢ o = m \cdot_{S} n \to o \underset{˙}{\cdot} Z = (m \cdot_{S} n) \underset{˙}{\cdot} Z$
30	29	eqeq2d	$⊢ o = m \cdot_{S} n \to (X = o \underset{˙}{\cdot} Z \leftrightarrow X = (m \cdot_{S} n) \underset{˙}{\cdot} Z)$
31	30	adantl	$⊢ ((((V \in LMod \land (X \underset{˙}{\sim} Y \land Y \underset{˙}{\sim} Z)) \land (m \in K \land X = m \underset{˙}{\cdot} Y)) \land (n \in K \land Y = n \underset{˙}{\cdot} Z)) \land o = m \cdot_{S} n) \to (X = o \underset{˙}{\cdot} Z \leftrightarrow X = (m \cdot_{S} n) \underset{˙}{\cdot} Z)$
32		simprr	$⊢ (((V \in LMod \land (X \underset{˙}{\sim} Y \land Y \underset{˙}{\sim} Z)) \land (m \in K \land X = m \underset{˙}{\cdot} Y)) \land (n \in K \land Y = n \underset{˙}{\cdot} Z)) \to Y = n \underset{˙}{\cdot} Z$
33	32	oveq2d	$⊢ (((V \in LMod \land (X \underset{˙}{\sim} Y \land Y \underset{˙}{\sim} Z)) \land (m \in K \land X = m \underset{˙}{\cdot} Y)) \land (n \in K \land Y = n \underset{˙}{\cdot} Z)) \to m \underset{˙}{\cdot} Y = m \underset{˙}{\cdot} (n \underset{˙}{\cdot} Z)$
34		simplrr	$⊢ (((V \in LMod \land (X \underset{˙}{\sim} Y \land Y \underset{˙}{\sim} Z)) \land (m \in K \land X = m \underset{˙}{\cdot} Y)) \land (n \in K \land Y = n \underset{˙}{\cdot} Z)) \to X = m \underset{˙}{\cdot} Y$
35		simplll	$⊢ (((V \in LMod \land (X \underset{˙}{\sim} Y \land Y \underset{˙}{\sim} Z)) \land (m \in K \land X = m \underset{˙}{\cdot} Y)) \land (n \in K \land Y = n \underset{˙}{\cdot} Z)) \to V \in LMod$
36		eldifi	$⊢ Z \in ({Base}_{V} ∖ \{0_{V}\}) \to Z \in {Base}_{V}$
37	36 2	eleq2s	$⊢ Z \in B \to Z \in {Base}_{V}$
38	21 37	syl	$⊢ (((V \in LMod \land (X \underset{˙}{\sim} Y \land Y \underset{˙}{\sim} Z)) \land (m \in K \land X = m \underset{˙}{\cdot} Y)) \land (n \in K \land Y = n \underset{˙}{\cdot} Z)) \to Z \in {Base}_{V}$
39		eqid	$⊢ {Base}_{V} = {Base}_{V}$
40	39 3 4 5 26	lmodvsass	$⊢ (V \in LMod \land (m \in K \land n \in K \land Z \in {Base}_{V})) \to (m \cdot_{S} n) \underset{˙}{\cdot} Z = m \underset{˙}{\cdot} (n \underset{˙}{\cdot} Z)$
41	35 24 25 38 40	syl13anc	$⊢ (((V \in LMod \land (X \underset{˙}{\sim} Y \land Y \underset{˙}{\sim} Z)) \land (m \in K \land X = m \underset{˙}{\cdot} Y)) \land (n \in K \land Y = n \underset{˙}{\cdot} Z)) \to (m \cdot_{S} n) \underset{˙}{\cdot} Z = m \underset{˙}{\cdot} (n \underset{˙}{\cdot} Z)$
42	33 34 41	3eqtr4d	$⊢ (((V \in LMod \land (X \underset{˙}{\sim} Y \land Y \underset{˙}{\sim} Z)) \land (m \in K \land X = m \underset{˙}{\cdot} Y)) \land (n \in K \land Y = n \underset{˙}{\cdot} Z)) \to X = (m \cdot_{S} n) \underset{˙}{\cdot} Z$
43	28 31 42	rspcedvd	$⊢ (((V \in LMod \land (X \underset{˙}{\sim} Y \land Y \underset{˙}{\sim} Z)) \land (m \in K \land X = m \underset{˙}{\cdot} Y)) \land (n \in K \land Y = n \underset{˙}{\cdot} Z)) \to \exists o \in K X = o \underset{˙}{\cdot} Z$
44	1	prjsprel	$⊢ X \underset{˙}{\sim} Z \leftrightarrow ((X \in B \land Z \in B) \land \exists o \in K X = o \underset{˙}{\cdot} Z)$
45	17 21 43 44	syl21anbrc	$⊢ (((V \in LMod \land (X \underset{˙}{\sim} Y \land Y \underset{˙}{\sim} Z)) \land (m \in K \land X = m \underset{˙}{\cdot} Y)) \land (n \in K \land Y = n \underset{˙}{\cdot} Z)) \to X \underset{˙}{\sim} Z$
46	12 45	rexlimddv	$⊢ ((V \in LMod \land (X \underset{˙}{\sim} Y \land Y \underset{˙}{\sim} Z)) \land (m \in K \land X = m \underset{˙}{\cdot} Y)) \to X \underset{˙}{\sim} Z$
47	8 46	rexlimddv	$⊢ (V \in LMod \land (X \underset{˙}{\sim} Y \land Y \underset{˙}{\sim} Z)) \to X \underset{˙}{\sim} Z$

Metamath Proof Explorer

Theorem prjspertr

Proof