Theorem prjspertr

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

	Ref	Expression
Hypotheses	prjsprel.1	⊢ ∼ = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ∧ ∃ 𝑙 ∈ 𝐾 𝑥 = ( 𝑙 · 𝑦 ) ) }
	prjspertr.b	⊢ 𝐵 = ( ( Base ‘ 𝑉 ) ∖ { ( 0g ‘ 𝑉 ) } )
	prjspertr.s	⊢ 𝑆 = ( Scalar ‘ 𝑉 )
	prjspertr.x	⊢ · = ( ·𝑠 ‘ 𝑉 )
	prjspertr.k	⊢ 𝐾 = ( Base ‘ 𝑆 )
Assertion	prjspertr	⊢ ( ( 𝑉 ∈ LMod ∧ ( 𝑋 ∼ 𝑌 ∧ 𝑌 ∼ 𝑍 ) ) → 𝑋 ∼ 𝑍 )

Proof

Step	Hyp	Ref	Expression
1		prjsprel.1	⊢ ∼ = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ∧ ∃ 𝑙 ∈ 𝐾 𝑥 = ( 𝑙 · 𝑦 ) ) }
2		prjspertr.b	⊢ 𝐵 = ( ( Base ‘ 𝑉 ) ∖ { ( 0g ‘ 𝑉 ) } )
3		prjspertr.s	⊢ 𝑆 = ( Scalar ‘ 𝑉 )
4		prjspertr.x	⊢ · = ( ·𝑠 ‘ 𝑉 )
5		prjspertr.k	⊢ 𝐾 = ( Base ‘ 𝑆 )
6	1	prjsprel	⊢ ( 𝑋 ∼ 𝑌 ↔ ( ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ ∃ 𝑚 ∈ 𝐾 𝑋 = ( 𝑚 · 𝑌 ) ) )
7	6	simprbi	⊢ ( 𝑋 ∼ 𝑌 → ∃ 𝑚 ∈ 𝐾 𝑋 = ( 𝑚 · 𝑌 ) )
8	7	ad2antrl	⊢ ( ( 𝑉 ∈ LMod ∧ ( 𝑋 ∼ 𝑌 ∧ 𝑌 ∼ 𝑍 ) ) → ∃ 𝑚 ∈ 𝐾 𝑋 = ( 𝑚 · 𝑌 ) )
9		simplrr	⊢ ( ( ( 𝑉 ∈ LMod ∧ ( 𝑋 ∼ 𝑌 ∧ 𝑌 ∼ 𝑍 ) ) ∧ ( 𝑚 ∈ 𝐾 ∧ 𝑋 = ( 𝑚 · 𝑌 ) ) ) → 𝑌 ∼ 𝑍 )
10	1	prjsprel	⊢ ( 𝑌 ∼ 𝑍 ↔ ( ( 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ∧ ∃ 𝑛 ∈ 𝐾 𝑌 = ( 𝑛 · 𝑍 ) ) )
11	10	simprbi	⊢ ( 𝑌 ∼ 𝑍 → ∃ 𝑛 ∈ 𝐾 𝑌 = ( 𝑛 · 𝑍 ) )
12	9 11	syl	⊢ ( ( ( 𝑉 ∈ LMod ∧ ( 𝑋 ∼ 𝑌 ∧ 𝑌 ∼ 𝑍 ) ) ∧ ( 𝑚 ∈ 𝐾 ∧ 𝑋 = ( 𝑚 · 𝑌 ) ) ) → ∃ 𝑛 ∈ 𝐾 𝑌 = ( 𝑛 · 𝑍 ) )
13		simplrl	⊢ ( ( ( 𝑉 ∈ LMod ∧ ( 𝑋 ∼ 𝑌 ∧ 𝑌 ∼ 𝑍 ) ) ∧ ( ( 𝑚 ∈ 𝐾 ∧ 𝑋 = ( 𝑚 · 𝑌 ) ) ∧ ( 𝑛 ∈ 𝐾 ∧ 𝑌 = ( 𝑛 · 𝑍 ) ) ) ) → 𝑋 ∼ 𝑌 )
14	13	anassrs	⊢ ( ( ( ( 𝑉 ∈ LMod ∧ ( 𝑋 ∼ 𝑌 ∧ 𝑌 ∼ 𝑍 ) ) ∧ ( 𝑚 ∈ 𝐾 ∧ 𝑋 = ( 𝑚 · 𝑌 ) ) ) ∧ ( 𝑛 ∈ 𝐾 ∧ 𝑌 = ( 𝑛 · 𝑍 ) ) ) → 𝑋 ∼ 𝑌 )
15		simpll	⊢ ( ( ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ ∃ 𝑚 ∈ 𝐾 𝑋 = ( 𝑚 · 𝑌 ) ) → 𝑋 ∈ 𝐵 )
16	6 15	sylbi	⊢ ( 𝑋 ∼ 𝑌 → 𝑋 ∈ 𝐵 )
17	14 16	syl	⊢ ( ( ( ( 𝑉 ∈ LMod ∧ ( 𝑋 ∼ 𝑌 ∧ 𝑌 ∼ 𝑍 ) ) ∧ ( 𝑚 ∈ 𝐾 ∧ 𝑋 = ( 𝑚 · 𝑌 ) ) ) ∧ ( 𝑛 ∈ 𝐾 ∧ 𝑌 = ( 𝑛 · 𝑍 ) ) ) → 𝑋 ∈ 𝐵 )
18	9	adantr	⊢ ( ( ( ( 𝑉 ∈ LMod ∧ ( 𝑋 ∼ 𝑌 ∧ 𝑌 ∼ 𝑍 ) ) ∧ ( 𝑚 ∈ 𝐾 ∧ 𝑋 = ( 𝑚 · 𝑌 ) ) ) ∧ ( 𝑛 ∈ 𝐾 ∧ 𝑌 = ( 𝑛 · 𝑍 ) ) ) → 𝑌 ∼ 𝑍 )
19		simplr	⊢ ( ( ( 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ∧ ∃ 𝑛 ∈ 𝐾 𝑌 = ( 𝑛 · 𝑍 ) ) → 𝑍 ∈ 𝐵 )
20	10 19	sylbi	⊢ ( 𝑌 ∼ 𝑍 → 𝑍 ∈ 𝐵 )
21	18 20	syl	⊢ ( ( ( ( 𝑉 ∈ LMod ∧ ( 𝑋 ∼ 𝑌 ∧ 𝑌 ∼ 𝑍 ) ) ∧ ( 𝑚 ∈ 𝐾 ∧ 𝑋 = ( 𝑚 · 𝑌 ) ) ) ∧ ( 𝑛 ∈ 𝐾 ∧ 𝑌 = ( 𝑛 · 𝑍 ) ) ) → 𝑍 ∈ 𝐵 )
22	3	lmodring	⊢ ( 𝑉 ∈ LMod → 𝑆 ∈ Ring )
23	22	ad3antrrr	⊢ ( ( ( ( 𝑉 ∈ LMod ∧ ( 𝑋 ∼ 𝑌 ∧ 𝑌 ∼ 𝑍 ) ) ∧ ( 𝑚 ∈ 𝐾 ∧ 𝑋 = ( 𝑚 · 𝑌 ) ) ) ∧ ( 𝑛 ∈ 𝐾 ∧ 𝑌 = ( 𝑛 · 𝑍 ) ) ) → 𝑆 ∈ Ring )
24		simplrl	⊢ ( ( ( ( 𝑉 ∈ LMod ∧ ( 𝑋 ∼ 𝑌 ∧ 𝑌 ∼ 𝑍 ) ) ∧ ( 𝑚 ∈ 𝐾 ∧ 𝑋 = ( 𝑚 · 𝑌 ) ) ) ∧ ( 𝑛 ∈ 𝐾 ∧ 𝑌 = ( 𝑛 · 𝑍 ) ) ) → 𝑚 ∈ 𝐾 )
25		simprl	⊢ ( ( ( ( 𝑉 ∈ LMod ∧ ( 𝑋 ∼ 𝑌 ∧ 𝑌 ∼ 𝑍 ) ) ∧ ( 𝑚 ∈ 𝐾 ∧ 𝑋 = ( 𝑚 · 𝑌 ) ) ) ∧ ( 𝑛 ∈ 𝐾 ∧ 𝑌 = ( 𝑛 · 𝑍 ) ) ) → 𝑛 ∈ 𝐾 )
26		eqid	⊢ ( .r ‘ 𝑆 ) = ( .r ‘ 𝑆 )
27	5 26	ringcl	⊢ ( ( 𝑆 ∈ Ring ∧ 𝑚 ∈ 𝐾 ∧ 𝑛 ∈ 𝐾 ) → ( 𝑚 ( .r ‘ 𝑆 ) 𝑛 ) ∈ 𝐾 )
28	23 24 25 27	syl3anc	⊢ ( ( ( ( 𝑉 ∈ LMod ∧ ( 𝑋 ∼ 𝑌 ∧ 𝑌 ∼ 𝑍 ) ) ∧ ( 𝑚 ∈ 𝐾 ∧ 𝑋 = ( 𝑚 · 𝑌 ) ) ) ∧ ( 𝑛 ∈ 𝐾 ∧ 𝑌 = ( 𝑛 · 𝑍 ) ) ) → ( 𝑚 ( .r ‘ 𝑆 ) 𝑛 ) ∈ 𝐾 )
29		oveq1	⊢ ( 𝑜 = ( 𝑚 ( .r ‘ 𝑆 ) 𝑛 ) → ( 𝑜 · 𝑍 ) = ( ( 𝑚 ( .r ‘ 𝑆 ) 𝑛 ) · 𝑍 ) )
30	29	eqeq2d	⊢ ( 𝑜 = ( 𝑚 ( .r ‘ 𝑆 ) 𝑛 ) → ( 𝑋 = ( 𝑜 · 𝑍 ) ↔ 𝑋 = ( ( 𝑚 ( .r ‘ 𝑆 ) 𝑛 ) · 𝑍 ) ) )
31	30	adantl	⊢ ( ( ( ( ( 𝑉 ∈ LMod ∧ ( 𝑋 ∼ 𝑌 ∧ 𝑌 ∼ 𝑍 ) ) ∧ ( 𝑚 ∈ 𝐾 ∧ 𝑋 = ( 𝑚 · 𝑌 ) ) ) ∧ ( 𝑛 ∈ 𝐾 ∧ 𝑌 = ( 𝑛 · 𝑍 ) ) ) ∧ 𝑜 = ( 𝑚 ( .r ‘ 𝑆 ) 𝑛 ) ) → ( 𝑋 = ( 𝑜 · 𝑍 ) ↔ 𝑋 = ( ( 𝑚 ( .r ‘ 𝑆 ) 𝑛 ) · 𝑍 ) ) )
32		simprr	⊢ ( ( ( ( 𝑉 ∈ LMod ∧ ( 𝑋 ∼ 𝑌 ∧ 𝑌 ∼ 𝑍 ) ) ∧ ( 𝑚 ∈ 𝐾 ∧ 𝑋 = ( 𝑚 · 𝑌 ) ) ) ∧ ( 𝑛 ∈ 𝐾 ∧ 𝑌 = ( 𝑛 · 𝑍 ) ) ) → 𝑌 = ( 𝑛 · 𝑍 ) )
33	32	oveq2d	⊢ ( ( ( ( 𝑉 ∈ LMod ∧ ( 𝑋 ∼ 𝑌 ∧ 𝑌 ∼ 𝑍 ) ) ∧ ( 𝑚 ∈ 𝐾 ∧ 𝑋 = ( 𝑚 · 𝑌 ) ) ) ∧ ( 𝑛 ∈ 𝐾 ∧ 𝑌 = ( 𝑛 · 𝑍 ) ) ) → ( 𝑚 · 𝑌 ) = ( 𝑚 · ( 𝑛 · 𝑍 ) ) )
34		simplrr	⊢ ( ( ( ( 𝑉 ∈ LMod ∧ ( 𝑋 ∼ 𝑌 ∧ 𝑌 ∼ 𝑍 ) ) ∧ ( 𝑚 ∈ 𝐾 ∧ 𝑋 = ( 𝑚 · 𝑌 ) ) ) ∧ ( 𝑛 ∈ 𝐾 ∧ 𝑌 = ( 𝑛 · 𝑍 ) ) ) → 𝑋 = ( 𝑚 · 𝑌 ) )
35		simplll	⊢ ( ( ( ( 𝑉 ∈ LMod ∧ ( 𝑋 ∼ 𝑌 ∧ 𝑌 ∼ 𝑍 ) ) ∧ ( 𝑚 ∈ 𝐾 ∧ 𝑋 = ( 𝑚 · 𝑌 ) ) ) ∧ ( 𝑛 ∈ 𝐾 ∧ 𝑌 = ( 𝑛 · 𝑍 ) ) ) → 𝑉 ∈ LMod )
36		eldifi	⊢ ( 𝑍 ∈ ( ( Base ‘ 𝑉 ) ∖ { ( 0g ‘ 𝑉 ) } ) → 𝑍 ∈ ( Base ‘ 𝑉 ) )
37	36 2	eleq2s	⊢ ( 𝑍 ∈ 𝐵 → 𝑍 ∈ ( Base ‘ 𝑉 ) )
38	21 37	syl	⊢ ( ( ( ( 𝑉 ∈ LMod ∧ ( 𝑋 ∼ 𝑌 ∧ 𝑌 ∼ 𝑍 ) ) ∧ ( 𝑚 ∈ 𝐾 ∧ 𝑋 = ( 𝑚 · 𝑌 ) ) ) ∧ ( 𝑛 ∈ 𝐾 ∧ 𝑌 = ( 𝑛 · 𝑍 ) ) ) → 𝑍 ∈ ( Base ‘ 𝑉 ) )
39		eqid	⊢ ( Base ‘ 𝑉 ) = ( Base ‘ 𝑉 )
40	39 3 4 5 26	lmodvsass	⊢ ( ( 𝑉 ∈ LMod ∧ ( 𝑚 ∈ 𝐾 ∧ 𝑛 ∈ 𝐾 ∧ 𝑍 ∈ ( Base ‘ 𝑉 ) ) ) → ( ( 𝑚 ( .r ‘ 𝑆 ) 𝑛 ) · 𝑍 ) = ( 𝑚 · ( 𝑛 · 𝑍 ) ) )
41	35 24 25 38 40	syl13anc	⊢ ( ( ( ( 𝑉 ∈ LMod ∧ ( 𝑋 ∼ 𝑌 ∧ 𝑌 ∼ 𝑍 ) ) ∧ ( 𝑚 ∈ 𝐾 ∧ 𝑋 = ( 𝑚 · 𝑌 ) ) ) ∧ ( 𝑛 ∈ 𝐾 ∧ 𝑌 = ( 𝑛 · 𝑍 ) ) ) → ( ( 𝑚 ( .r ‘ 𝑆 ) 𝑛 ) · 𝑍 ) = ( 𝑚 · ( 𝑛 · 𝑍 ) ) )
42	33 34 41	3eqtr4d	⊢ ( ( ( ( 𝑉 ∈ LMod ∧ ( 𝑋 ∼ 𝑌 ∧ 𝑌 ∼ 𝑍 ) ) ∧ ( 𝑚 ∈ 𝐾 ∧ 𝑋 = ( 𝑚 · 𝑌 ) ) ) ∧ ( 𝑛 ∈ 𝐾 ∧ 𝑌 = ( 𝑛 · 𝑍 ) ) ) → 𝑋 = ( ( 𝑚 ( .r ‘ 𝑆 ) 𝑛 ) · 𝑍 ) )
43	28 31 42	rspcedvd	⊢ ( ( ( ( 𝑉 ∈ LMod ∧ ( 𝑋 ∼ 𝑌 ∧ 𝑌 ∼ 𝑍 ) ) ∧ ( 𝑚 ∈ 𝐾 ∧ 𝑋 = ( 𝑚 · 𝑌 ) ) ) ∧ ( 𝑛 ∈ 𝐾 ∧ 𝑌 = ( 𝑛 · 𝑍 ) ) ) → ∃ 𝑜 ∈ 𝐾 𝑋 = ( 𝑜 · 𝑍 ) )
44	1	prjsprel	⊢ ( 𝑋 ∼ 𝑍 ↔ ( ( 𝑋 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ∧ ∃ 𝑜 ∈ 𝐾 𝑋 = ( 𝑜 · 𝑍 ) ) )
45	17 21 43 44	syl21anbrc	⊢ ( ( ( ( 𝑉 ∈ LMod ∧ ( 𝑋 ∼ 𝑌 ∧ 𝑌 ∼ 𝑍 ) ) ∧ ( 𝑚 ∈ 𝐾 ∧ 𝑋 = ( 𝑚 · 𝑌 ) ) ) ∧ ( 𝑛 ∈ 𝐾 ∧ 𝑌 = ( 𝑛 · 𝑍 ) ) ) → 𝑋 ∼ 𝑍 )
46	12 45	rexlimddv	⊢ ( ( ( 𝑉 ∈ LMod ∧ ( 𝑋 ∼ 𝑌 ∧ 𝑌 ∼ 𝑍 ) ) ∧ ( 𝑚 ∈ 𝐾 ∧ 𝑋 = ( 𝑚 · 𝑌 ) ) ) → 𝑋 ∼ 𝑍 )
47	8 46	rexlimddv	⊢ ( ( 𝑉 ∈ LMod ∧ ( 𝑋 ∼ 𝑌 ∧ 𝑌 ∼ 𝑍 ) ) → 𝑋 ∼ 𝑍 )