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		oveq1	⊢ ( 𝑜 = ( 𝑚 ( .r ‘ 𝑆 ) 𝑛 ) → ( 𝑜 · 𝑍 ) = ( ( 𝑚 ( .r ‘ 𝑆 ) 𝑛 ) · 𝑍 ) )
23	22	eqeq2d	⊢ ( 𝑜 = ( 𝑚 ( .r ‘ 𝑆 ) 𝑛 ) → ( 𝑋 = ( 𝑜 · 𝑍 ) ↔ 𝑋 = ( ( 𝑚 ( .r ‘ 𝑆 ) 𝑛 ) · 𝑍 ) ) )
24		eqid	⊢ ( .r ‘ 𝑆 ) = ( .r ‘ 𝑆 )
25	3	lmodring	⊢ ( 𝑉 ∈ LMod → 𝑆 ∈ Ring )
26	25	ad3antrrr	⊢ ( ( ( ( 𝑉 ∈ LMod ∧ ( 𝑋 ∼ 𝑌 ∧ 𝑌 ∼ 𝑍 ) ) ∧ ( 𝑚 ∈ 𝐾 ∧ 𝑋 = ( 𝑚 · 𝑌 ) ) ) ∧ ( 𝑛 ∈ 𝐾 ∧ 𝑌 = ( 𝑛 · 𝑍 ) ) ) → 𝑆 ∈ Ring )
27		simplrl	⊢ ( ( ( ( 𝑉 ∈ LMod ∧ ( 𝑋 ∼ 𝑌 ∧ 𝑌 ∼ 𝑍 ) ) ∧ ( 𝑚 ∈ 𝐾 ∧ 𝑋 = ( 𝑚 · 𝑌 ) ) ) ∧ ( 𝑛 ∈ 𝐾 ∧ 𝑌 = ( 𝑛 · 𝑍 ) ) ) → 𝑚 ∈ 𝐾 )
28		simprl	⊢ ( ( ( ( 𝑉 ∈ LMod ∧ ( 𝑋 ∼ 𝑌 ∧ 𝑌 ∼ 𝑍 ) ) ∧ ( 𝑚 ∈ 𝐾 ∧ 𝑋 = ( 𝑚 · 𝑌 ) ) ) ∧ ( 𝑛 ∈ 𝐾 ∧ 𝑌 = ( 𝑛 · 𝑍 ) ) ) → 𝑛 ∈ 𝐾 )
29	5 24 26 27 28	ringcld	⊢ ( ( ( ( 𝑉 ∈ LMod ∧ ( 𝑋 ∼ 𝑌 ∧ 𝑌 ∼ 𝑍 ) ) ∧ ( 𝑚 ∈ 𝐾 ∧ 𝑋 = ( 𝑚 · 𝑌 ) ) ) ∧ ( 𝑛 ∈ 𝐾 ∧ 𝑌 = ( 𝑛 · 𝑍 ) ) ) → ( 𝑚 ( .r ‘ 𝑆 ) 𝑛 ) ∈ 𝐾 )
30		simprr	⊢ ( ( ( ( 𝑉 ∈ LMod ∧ ( 𝑋 ∼ 𝑌 ∧ 𝑌 ∼ 𝑍 ) ) ∧ ( 𝑚 ∈ 𝐾 ∧ 𝑋 = ( 𝑚 · 𝑌 ) ) ) ∧ ( 𝑛 ∈ 𝐾 ∧ 𝑌 = ( 𝑛 · 𝑍 ) ) ) → 𝑌 = ( 𝑛 · 𝑍 ) )
31	30	oveq2d	⊢ ( ( ( ( 𝑉 ∈ LMod ∧ ( 𝑋 ∼ 𝑌 ∧ 𝑌 ∼ 𝑍 ) ) ∧ ( 𝑚 ∈ 𝐾 ∧ 𝑋 = ( 𝑚 · 𝑌 ) ) ) ∧ ( 𝑛 ∈ 𝐾 ∧ 𝑌 = ( 𝑛 · 𝑍 ) ) ) → ( 𝑚 · 𝑌 ) = ( 𝑚 · ( 𝑛 · 𝑍 ) ) )
32		simplrr	⊢ ( ( ( ( 𝑉 ∈ LMod ∧ ( 𝑋 ∼ 𝑌 ∧ 𝑌 ∼ 𝑍 ) ) ∧ ( 𝑚 ∈ 𝐾 ∧ 𝑋 = ( 𝑚 · 𝑌 ) ) ) ∧ ( 𝑛 ∈ 𝐾 ∧ 𝑌 = ( 𝑛 · 𝑍 ) ) ) → 𝑋 = ( 𝑚 · 𝑌 ) )
33		simplll	⊢ ( ( ( ( 𝑉 ∈ LMod ∧ ( 𝑋 ∼ 𝑌 ∧ 𝑌 ∼ 𝑍 ) ) ∧ ( 𝑚 ∈ 𝐾 ∧ 𝑋 = ( 𝑚 · 𝑌 ) ) ) ∧ ( 𝑛 ∈ 𝐾 ∧ 𝑌 = ( 𝑛 · 𝑍 ) ) ) → 𝑉 ∈ LMod )
34		eldifi	⊢ ( 𝑍 ∈ ( ( Base ‘ 𝑉 ) ∖ { ( 0g ‘ 𝑉 ) } ) → 𝑍 ∈ ( Base ‘ 𝑉 ) )
35	34 2	eleq2s	⊢ ( 𝑍 ∈ 𝐵 → 𝑍 ∈ ( Base ‘ 𝑉 ) )
36	21 35	syl	⊢ ( ( ( ( 𝑉 ∈ LMod ∧ ( 𝑋 ∼ 𝑌 ∧ 𝑌 ∼ 𝑍 ) ) ∧ ( 𝑚 ∈ 𝐾 ∧ 𝑋 = ( 𝑚 · 𝑌 ) ) ) ∧ ( 𝑛 ∈ 𝐾 ∧ 𝑌 = ( 𝑛 · 𝑍 ) ) ) → 𝑍 ∈ ( Base ‘ 𝑉 ) )
37		eqid	⊢ ( Base ‘ 𝑉 ) = ( Base ‘ 𝑉 )
38	37 3 4 5 24	lmodvsass	⊢ ( ( 𝑉 ∈ LMod ∧ ( 𝑚 ∈ 𝐾 ∧ 𝑛 ∈ 𝐾 ∧ 𝑍 ∈ ( Base ‘ 𝑉 ) ) ) → ( ( 𝑚 ( .r ‘ 𝑆 ) 𝑛 ) · 𝑍 ) = ( 𝑚 · ( 𝑛 · 𝑍 ) ) )
39	33 27 28 36 38	syl13anc	⊢ ( ( ( ( 𝑉 ∈ LMod ∧ ( 𝑋 ∼ 𝑌 ∧ 𝑌 ∼ 𝑍 ) ) ∧ ( 𝑚 ∈ 𝐾 ∧ 𝑋 = ( 𝑚 · 𝑌 ) ) ) ∧ ( 𝑛 ∈ 𝐾 ∧ 𝑌 = ( 𝑛 · 𝑍 ) ) ) → ( ( 𝑚 ( .r ‘ 𝑆 ) 𝑛 ) · 𝑍 ) = ( 𝑚 · ( 𝑛 · 𝑍 ) ) )
40	31 32 39	3eqtr4d	⊢ ( ( ( ( 𝑉 ∈ LMod ∧ ( 𝑋 ∼ 𝑌 ∧ 𝑌 ∼ 𝑍 ) ) ∧ ( 𝑚 ∈ 𝐾 ∧ 𝑋 = ( 𝑚 · 𝑌 ) ) ) ∧ ( 𝑛 ∈ 𝐾 ∧ 𝑌 = ( 𝑛 · 𝑍 ) ) ) → 𝑋 = ( ( 𝑚 ( .r ‘ 𝑆 ) 𝑛 ) · 𝑍 ) )
41	23 29 40	rspcedvdw	⊢ ( ( ( ( 𝑉 ∈ LMod ∧ ( 𝑋 ∼ 𝑌 ∧ 𝑌 ∼ 𝑍 ) ) ∧ ( 𝑚 ∈ 𝐾 ∧ 𝑋 = ( 𝑚 · 𝑌 ) ) ) ∧ ( 𝑛 ∈ 𝐾 ∧ 𝑌 = ( 𝑛 · 𝑍 ) ) ) → ∃ 𝑜 ∈ 𝐾 𝑋 = ( 𝑜 · 𝑍 ) )
42	1	prjsprel	⊢ ( 𝑋 ∼ 𝑍 ↔ ( ( 𝑋 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ∧ ∃ 𝑜 ∈ 𝐾 𝑋 = ( 𝑜 · 𝑍 ) ) )
43	17 21 41 42	syl21anbrc	⊢ ( ( ( ( 𝑉 ∈ LMod ∧ ( 𝑋 ∼ 𝑌 ∧ 𝑌 ∼ 𝑍 ) ) ∧ ( 𝑚 ∈ 𝐾 ∧ 𝑋 = ( 𝑚 · 𝑌 ) ) ) ∧ ( 𝑛 ∈ 𝐾 ∧ 𝑌 = ( 𝑛 · 𝑍 ) ) ) → 𝑋 ∼ 𝑍 )
44	12 43	rexlimddv	⊢ ( ( ( 𝑉 ∈ LMod ∧ ( 𝑋 ∼ 𝑌 ∧ 𝑌 ∼ 𝑍 ) ) ∧ ( 𝑚 ∈ 𝐾 ∧ 𝑋 = ( 𝑚 · 𝑌 ) ) ) → 𝑋 ∼ 𝑍 )
45	8 44	rexlimddv	⊢ ( ( 𝑉 ∈ LMod ∧ ( 𝑋 ∼ 𝑌 ∧ 𝑌 ∼ 𝑍 ) ) → 𝑋 ∼ 𝑍 )