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		oveq1	$⊢ o = m \cdot_{S} n \to o \underset{˙}{\cdot} Z = (m \cdot_{S} n) \underset{˙}{\cdot} Z$
23	22	eqeq2d	$⊢ o = m \cdot_{S} n \to (X = o \underset{˙}{\cdot} Z \leftrightarrow X = (m \cdot_{S} n) \underset{˙}{\cdot} Z)$
24		eqid	$⊢ \cdot_{S} = \cdot_{S}$
25	3	lmodring	$⊢ V \in LMod \to S \in Ring$
26	25	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$
27		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$
28		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$
29	5 24 26 27 28	ringcld	$⊢ (((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$
30		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$
31	30	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)$
32		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$
33		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$
34		eldifi	$⊢ Z \in ({Base}_{V} ∖ \{0_{V}\}) \to Z \in {Base}_{V}$
35	34 2	eleq2s	$⊢ Z \in B \to Z \in {Base}_{V}$
36	21 35	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}$
37		eqid	$⊢ {Base}_{V} = {Base}_{V}$
38	37 3 4 5 24	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)$
39	33 27 28 36 38	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)$
40	31 32 39	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$
41	23 29 40	rspcedvdw	$⊢ (((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$
42	1	prjsprel	$⊢ X \underset{˙}{\sim} Z \leftrightarrow ((X \in B \land Z \in B) \land \exists o \in K X = o \underset{˙}{\cdot} Z)$
43	17 21 41 42	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$
44	12 43	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$
45	8 44	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