Theorem lmod1

Description: The (smallest) structure representing azero module over an arbitrary ring. (Contributed by AV, 29-Apr-2019)

	Ref	Expression
Hypothesis	lmod1.m	⊢ 𝑀 = ( { ⟨ ( Base ‘ ndx ) , { 𝐼 } ⟩ , ⟨ ( +g ‘ ndx ) , { ⟨ ⟨ 𝐼 , 𝐼 ⟩ , 𝐼 ⟩ } ⟩ , ⟨ ( Scalar ‘ ndx ) , 𝑅 ⟩ } ∪ { ⟨ ( ·𝑠 ‘ ndx ) , ( 𝑥 ∈ ( Base ‘ 𝑅 ) , 𝑦 ∈ { 𝐼 } ↦ 𝑦 ) ⟩ } )
Assertion	lmod1	⊢ ( ( 𝐼 ∈ 𝑉 ∧ 𝑅 ∈ Ring ) → 𝑀 ∈ LMod )

Proof

Step	Hyp	Ref	Expression
1		lmod1.m	⊢ 𝑀 = ( { ⟨ ( Base ‘ ndx ) , { 𝐼 } ⟩ , ⟨ ( +g ‘ ndx ) , { ⟨ ⟨ 𝐼 , 𝐼 ⟩ , 𝐼 ⟩ } ⟩ , ⟨ ( Scalar ‘ ndx ) , 𝑅 ⟩ } ∪ { ⟨ ( ·𝑠 ‘ ndx ) , ( 𝑥 ∈ ( Base ‘ 𝑅 ) , 𝑦 ∈ { 𝐼 } ↦ 𝑦 ) ⟩ } )
2		eqid	⊢ { ⟨ ( Base ‘ ndx ) , { 𝐼 } ⟩ , ⟨ ( +g ‘ ndx ) , { ⟨ ⟨ 𝐼 , 𝐼 ⟩ , 𝐼 ⟩ } ⟩ } = { ⟨ ( Base ‘ ndx ) , { 𝐼 } ⟩ , ⟨ ( +g ‘ ndx ) , { ⟨ ⟨ 𝐼 , 𝐼 ⟩ , 𝐼 ⟩ } ⟩ }
3	2	grp1	⊢ ( 𝐼 ∈ 𝑉 → { ⟨ ( Base ‘ ndx ) , { 𝐼 } ⟩ , ⟨ ( +g ‘ ndx ) , { ⟨ ⟨ 𝐼 , 𝐼 ⟩ , 𝐼 ⟩ } ⟩ } ∈ Grp )
4		fvex	⊢ ( Base ‘ { ⟨ ( Base ‘ ndx ) , { 𝐼 } ⟩ , ⟨ ( +g ‘ ndx ) , { ⟨ ⟨ 𝐼 , 𝐼 ⟩ , 𝐼 ⟩ } ⟩ } ) ∈ V
5		snex	⊢ { 𝐼 } ∈ V
6	2	grpbase	⊢ ( { 𝐼 } ∈ V → { 𝐼 } = ( Base ‘ { ⟨ ( Base ‘ ndx ) , { 𝐼 } ⟩ , ⟨ ( +g ‘ ndx ) , { ⟨ ⟨ 𝐼 , 𝐼 ⟩ , 𝐼 ⟩ } ⟩ } ) )
7	5 6	ax-mp	⊢ { 𝐼 } = ( Base ‘ { ⟨ ( Base ‘ ndx ) , { 𝐼 } ⟩ , ⟨ ( +g ‘ ndx ) , { ⟨ ⟨ 𝐼 , 𝐼 ⟩ , 𝐼 ⟩ } ⟩ } )
8	7	opeq2i	⊢ ⟨ ( Base ‘ ndx ) , { 𝐼 } ⟩ = ⟨ ( Base ‘ ndx ) , ( Base ‘ { ⟨ ( Base ‘ ndx ) , { 𝐼 } ⟩ , ⟨ ( +g ‘ ndx ) , { ⟨ ⟨ 𝐼 , 𝐼 ⟩ , 𝐼 ⟩ } ⟩ } ) ⟩
9		tpeq1	⊢ ( ⟨ ( Base ‘ ndx ) , { 𝐼 } ⟩ = ⟨ ( Base ‘ ndx ) , ( Base ‘ { ⟨ ( Base ‘ ndx ) , { 𝐼 } ⟩ , ⟨ ( +g ‘ ndx ) , { ⟨ ⟨ 𝐼 , 𝐼 ⟩ , 𝐼 ⟩ } ⟩ } ) ⟩ → { ⟨ ( Base ‘ ndx ) , { 𝐼 } ⟩ , ⟨ ( +g ‘ ndx ) , { ⟨ ⟨ 𝐼 , 𝐼 ⟩ , 𝐼 ⟩ } ⟩ , ⟨ ( Scalar ‘ ndx ) , 𝑅 ⟩ } = { ⟨ ( Base ‘ ndx ) , ( Base ‘ { ⟨ ( Base ‘ ndx ) , { 𝐼 } ⟩ , ⟨ ( +g ‘ ndx ) , { ⟨ ⟨ 𝐼 , 𝐼 ⟩ , 𝐼 ⟩ } ⟩ } ) ⟩ , ⟨ ( +g ‘ ndx ) , { ⟨ ⟨ 𝐼 , 𝐼 ⟩ , 𝐼 ⟩ } ⟩ , ⟨ ( Scalar ‘ ndx ) , 𝑅 ⟩ } )
10	8 9	ax-mp	⊢ { ⟨ ( Base ‘ ndx ) , { 𝐼 } ⟩ , ⟨ ( +g ‘ ndx ) , { ⟨ ⟨ 𝐼 , 𝐼 ⟩ , 𝐼 ⟩ } ⟩ , ⟨ ( Scalar ‘ ndx ) , 𝑅 ⟩ } = { ⟨ ( Base ‘ ndx ) , ( Base ‘ { ⟨ ( Base ‘ ndx ) , { 𝐼 } ⟩ , ⟨ ( +g ‘ ndx ) , { ⟨ ⟨ 𝐼 , 𝐼 ⟩ , 𝐼 ⟩ } ⟩ } ) ⟩ , ⟨ ( +g ‘ ndx ) , { ⟨ ⟨ 𝐼 , 𝐼 ⟩ , 𝐼 ⟩ } ⟩ , ⟨ ( Scalar ‘ ndx ) , 𝑅 ⟩ }
11	10	uneq1i	⊢ ( { ⟨ ( Base ‘ ndx ) , { 𝐼 } ⟩ , ⟨ ( +g ‘ ndx ) , { ⟨ ⟨ 𝐼 , 𝐼 ⟩ , 𝐼 ⟩ } ⟩ , ⟨ ( Scalar ‘ ndx ) , 𝑅 ⟩ } ∪ { ⟨ ( ·𝑠 ‘ ndx ) , ( 𝑥 ∈ ( Base ‘ 𝑅 ) , 𝑦 ∈ { 𝐼 } ↦ 𝑦 ) ⟩ } ) = ( { ⟨ ( Base ‘ ndx ) , ( Base ‘ { ⟨ ( Base ‘ ndx ) , { 𝐼 } ⟩ , ⟨ ( +g ‘ ndx ) , { ⟨ ⟨ 𝐼 , 𝐼 ⟩ , 𝐼 ⟩ } ⟩ } ) ⟩ , ⟨ ( +g ‘ ndx ) , { ⟨ ⟨ 𝐼 , 𝐼 ⟩ , 𝐼 ⟩ } ⟩ , ⟨ ( Scalar ‘ ndx ) , 𝑅 ⟩ } ∪ { ⟨ ( ·𝑠 ‘ ndx ) , ( 𝑥 ∈ ( Base ‘ 𝑅 ) , 𝑦 ∈ { 𝐼 } ↦ 𝑦 ) ⟩ } )
12	1 11	eqtri	⊢ 𝑀 = ( { ⟨ ( Base ‘ ndx ) , ( Base ‘ { ⟨ ( Base ‘ ndx ) , { 𝐼 } ⟩ , ⟨ ( +g ‘ ndx ) , { ⟨ ⟨ 𝐼 , 𝐼 ⟩ , 𝐼 ⟩ } ⟩ } ) ⟩ , ⟨ ( +g ‘ ndx ) , { ⟨ ⟨ 𝐼 , 𝐼 ⟩ , 𝐼 ⟩ } ⟩ , ⟨ ( Scalar ‘ ndx ) , 𝑅 ⟩ } ∪ { ⟨ ( ·𝑠 ‘ ndx ) , ( 𝑥 ∈ ( Base ‘ 𝑅 ) , 𝑦 ∈ { 𝐼 } ↦ 𝑦 ) ⟩ } )
13	12	lmodbase	⊢ ( ( Base ‘ { ⟨ ( Base ‘ ndx ) , { 𝐼 } ⟩ , ⟨ ( +g ‘ ndx ) , { ⟨ ⟨ 𝐼 , 𝐼 ⟩ , 𝐼 ⟩ } ⟩ } ) ∈ V → ( Base ‘ { ⟨ ( Base ‘ ndx ) , { 𝐼 } ⟩ , ⟨ ( +g ‘ ndx ) , { ⟨ ⟨ 𝐼 , 𝐼 ⟩ , 𝐼 ⟩ } ⟩ } ) = ( Base ‘ 𝑀 ) )
14	4 13	ax-mp	⊢ ( Base ‘ { ⟨ ( Base ‘ ndx ) , { 𝐼 } ⟩ , ⟨ ( +g ‘ ndx ) , { ⟨ ⟨ 𝐼 , 𝐼 ⟩ , 𝐼 ⟩ } ⟩ } ) = ( Base ‘ 𝑀 )
15	14	eqcomi	⊢ ( Base ‘ 𝑀 ) = ( Base ‘ { ⟨ ( Base ‘ ndx ) , { 𝐼 } ⟩ , ⟨ ( +g ‘ ndx ) , { ⟨ ⟨ 𝐼 , 𝐼 ⟩ , 𝐼 ⟩ } ⟩ } )
16		fvex	⊢ ( +g ‘ { ⟨ ( Base ‘ ndx ) , { 𝐼 } ⟩ , ⟨ ( +g ‘ ndx ) , { ⟨ ⟨ 𝐼 , 𝐼 ⟩ , 𝐼 ⟩ } ⟩ } ) ∈ V
17		snex	⊢ { ⟨ ⟨ 𝐼 , 𝐼 ⟩ , 𝐼 ⟩ } ∈ V
18	2	grpplusg	⊢ ( { ⟨ ⟨ 𝐼 , 𝐼 ⟩ , 𝐼 ⟩ } ∈ V → { ⟨ ⟨ 𝐼 , 𝐼 ⟩ , 𝐼 ⟩ } = ( +g ‘ { ⟨ ( Base ‘ ndx ) , { 𝐼 } ⟩ , ⟨ ( +g ‘ ndx ) , { ⟨ ⟨ 𝐼 , 𝐼 ⟩ , 𝐼 ⟩ } ⟩ } ) )
19	17 18	ax-mp	⊢ { ⟨ ⟨ 𝐼 , 𝐼 ⟩ , 𝐼 ⟩ } = ( +g ‘ { ⟨ ( Base ‘ ndx ) , { 𝐼 } ⟩ , ⟨ ( +g ‘ ndx ) , { ⟨ ⟨ 𝐼 , 𝐼 ⟩ , 𝐼 ⟩ } ⟩ } )
20	19	opeq2i	⊢ ⟨ ( +g ‘ ndx ) , { ⟨ ⟨ 𝐼 , 𝐼 ⟩ , 𝐼 ⟩ } ⟩ = ⟨ ( +g ‘ ndx ) , ( +g ‘ { ⟨ ( Base ‘ ndx ) , { 𝐼 } ⟩ , ⟨ ( +g ‘ ndx ) , { ⟨ ⟨ 𝐼 , 𝐼 ⟩ , 𝐼 ⟩ } ⟩ } ) ⟩
21		tpeq2	⊢ ( ⟨ ( +g ‘ ndx ) , { ⟨ ⟨ 𝐼 , 𝐼 ⟩ , 𝐼 ⟩ } ⟩ = ⟨ ( +g ‘ ndx ) , ( +g ‘ { ⟨ ( Base ‘ ndx ) , { 𝐼 } ⟩ , ⟨ ( +g ‘ ndx ) , { ⟨ ⟨ 𝐼 , 𝐼 ⟩ , 𝐼 ⟩ } ⟩ } ) ⟩ → { ⟨ ( Base ‘ ndx ) , { 𝐼 } ⟩ , ⟨ ( +g ‘ ndx ) , { ⟨ ⟨ 𝐼 , 𝐼 ⟩ , 𝐼 ⟩ } ⟩ , ⟨ ( Scalar ‘ ndx ) , 𝑅 ⟩ } = { ⟨ ( Base ‘ ndx ) , { 𝐼 } ⟩ , ⟨ ( +g ‘ ndx ) , ( +g ‘ { ⟨ ( Base ‘ ndx ) , { 𝐼 } ⟩ , ⟨ ( +g ‘ ndx ) , { ⟨ ⟨ 𝐼 , 𝐼 ⟩ , 𝐼 ⟩ } ⟩ } ) ⟩ , ⟨ ( Scalar ‘ ndx ) , 𝑅 ⟩ } )
22	20 21	ax-mp	⊢ { ⟨ ( Base ‘ ndx ) , { 𝐼 } ⟩ , ⟨ ( +g ‘ ndx ) , { ⟨ ⟨ 𝐼 , 𝐼 ⟩ , 𝐼 ⟩ } ⟩ , ⟨ ( Scalar ‘ ndx ) , 𝑅 ⟩ } = { ⟨ ( Base ‘ ndx ) , { 𝐼 } ⟩ , ⟨ ( +g ‘ ndx ) , ( +g ‘ { ⟨ ( Base ‘ ndx ) , { 𝐼 } ⟩ , ⟨ ( +g ‘ ndx ) , { ⟨ ⟨ 𝐼 , 𝐼 ⟩ , 𝐼 ⟩ } ⟩ } ) ⟩ , ⟨ ( Scalar ‘ ndx ) , 𝑅 ⟩ }
23	22	uneq1i	⊢ ( { ⟨ ( Base ‘ ndx ) , { 𝐼 } ⟩ , ⟨ ( +g ‘ ndx ) , { ⟨ ⟨ 𝐼 , 𝐼 ⟩ , 𝐼 ⟩ } ⟩ , ⟨ ( Scalar ‘ ndx ) , 𝑅 ⟩ } ∪ { ⟨ ( ·𝑠 ‘ ndx ) , ( 𝑥 ∈ ( Base ‘ 𝑅 ) , 𝑦 ∈ { 𝐼 } ↦ 𝑦 ) ⟩ } ) = ( { ⟨ ( Base ‘ ndx ) , { 𝐼 } ⟩ , ⟨ ( +g ‘ ndx ) , ( +g ‘ { ⟨ ( Base ‘ ndx ) , { 𝐼 } ⟩ , ⟨ ( +g ‘ ndx ) , { ⟨ ⟨ 𝐼 , 𝐼 ⟩ , 𝐼 ⟩ } ⟩ } ) ⟩ , ⟨ ( Scalar ‘ ndx ) , 𝑅 ⟩ } ∪ { ⟨ ( ·𝑠 ‘ ndx ) , ( 𝑥 ∈ ( Base ‘ 𝑅 ) , 𝑦 ∈ { 𝐼 } ↦ 𝑦 ) ⟩ } )
24	1 23	eqtri	⊢ 𝑀 = ( { ⟨ ( Base ‘ ndx ) , { 𝐼 } ⟩ , ⟨ ( +g ‘ ndx ) , ( +g ‘ { ⟨ ( Base ‘ ndx ) , { 𝐼 } ⟩ , ⟨ ( +g ‘ ndx ) , { ⟨ ⟨ 𝐼 , 𝐼 ⟩ , 𝐼 ⟩ } ⟩ } ) ⟩ , ⟨ ( Scalar ‘ ndx ) , 𝑅 ⟩ } ∪ { ⟨ ( ·𝑠 ‘ ndx ) , ( 𝑥 ∈ ( Base ‘ 𝑅 ) , 𝑦 ∈ { 𝐼 } ↦ 𝑦 ) ⟩ } )
25	24	lmodplusg	⊢ ( ( +g ‘ { ⟨ ( Base ‘ ndx ) , { 𝐼 } ⟩ , ⟨ ( +g ‘ ndx ) , { ⟨ ⟨ 𝐼 , 𝐼 ⟩ , 𝐼 ⟩ } ⟩ } ) ∈ V → ( +g ‘ { ⟨ ( Base ‘ ndx ) , { 𝐼 } ⟩ , ⟨ ( +g ‘ ndx ) , { ⟨ ⟨ 𝐼 , 𝐼 ⟩ , 𝐼 ⟩ } ⟩ } ) = ( +g ‘ 𝑀 ) )
26	16 25	ax-mp	⊢ ( +g ‘ { ⟨ ( Base ‘ ndx ) , { 𝐼 } ⟩ , ⟨ ( +g ‘ ndx ) , { ⟨ ⟨ 𝐼 , 𝐼 ⟩ , 𝐼 ⟩ } ⟩ } ) = ( +g ‘ 𝑀 )
27	26	eqcomi	⊢ ( +g ‘ 𝑀 ) = ( +g ‘ { ⟨ ( Base ‘ ndx ) , { 𝐼 } ⟩ , ⟨ ( +g ‘ ndx ) , { ⟨ ⟨ 𝐼 , 𝐼 ⟩ , 𝐼 ⟩ } ⟩ } )
28	15 27	grpprop	⊢ ( 𝑀 ∈ Grp ↔ { ⟨ ( Base ‘ ndx ) , { 𝐼 } ⟩ , ⟨ ( +g ‘ ndx ) , { ⟨ ⟨ 𝐼 , 𝐼 ⟩ , 𝐼 ⟩ } ⟩ } ∈ Grp )
29	3 28	sylibr	⊢ ( 𝐼 ∈ 𝑉 → 𝑀 ∈ Grp )
30	29	adantr	⊢ ( ( 𝐼 ∈ 𝑉 ∧ 𝑅 ∈ Ring ) → 𝑀 ∈ Grp )
31	1	lmodsca	⊢ ( 𝑅 ∈ Ring → 𝑅 = ( Scalar ‘ 𝑀 ) )
32	31	eqcomd	⊢ ( 𝑅 ∈ Ring → ( Scalar ‘ 𝑀 ) = 𝑅 )
33	32	adantl	⊢ ( ( 𝐼 ∈ 𝑉 ∧ 𝑅 ∈ Ring ) → ( Scalar ‘ 𝑀 ) = 𝑅 )
34		simpr	⊢ ( ( 𝐼 ∈ 𝑉 ∧ 𝑅 ∈ Ring ) → 𝑅 ∈ Ring )
35	33 34	eqeltrd	⊢ ( ( 𝐼 ∈ 𝑉 ∧ 𝑅 ∈ Ring ) → ( Scalar ‘ 𝑀 ) ∈ Ring )
36	33	fveq2d	⊢ ( ( 𝐼 ∈ 𝑉 ∧ 𝑅 ∈ Ring ) → ( Base ‘ ( Scalar ‘ 𝑀 ) ) = ( Base ‘ 𝑅 ) )
37	36	eleq2d	⊢ ( ( 𝐼 ∈ 𝑉 ∧ 𝑅 ∈ Ring ) → ( 𝑞 ∈ ( Base ‘ ( Scalar ‘ 𝑀 ) ) ↔ 𝑞 ∈ ( Base ‘ 𝑅 ) ) )
38	36	eleq2d	⊢ ( ( 𝐼 ∈ 𝑉 ∧ 𝑅 ∈ Ring ) → ( 𝑟 ∈ ( Base ‘ ( Scalar ‘ 𝑀 ) ) ↔ 𝑟 ∈ ( Base ‘ 𝑅 ) ) )
39	37 38	anbi12d	⊢ ( ( 𝐼 ∈ 𝑉 ∧ 𝑅 ∈ Ring ) → ( ( 𝑞 ∈ ( Base ‘ ( Scalar ‘ 𝑀 ) ) ∧ 𝑟 ∈ ( Base ‘ ( Scalar ‘ 𝑀 ) ) ) ↔ ( 𝑞 ∈ ( Base ‘ 𝑅 ) ∧ 𝑟 ∈ ( Base ‘ 𝑅 ) ) ) )
40		simpll	⊢ ( ( ( 𝐼 ∈ 𝑉 ∧ 𝑅 ∈ Ring ) ∧ ( 𝑞 ∈ ( Base ‘ 𝑅 ) ∧ 𝑟 ∈ ( Base ‘ 𝑅 ) ) ) → 𝐼 ∈ 𝑉 )
41		simplr	⊢ ( ( ( 𝐼 ∈ 𝑉 ∧ 𝑅 ∈ Ring ) ∧ ( 𝑞 ∈ ( Base ‘ 𝑅 ) ∧ 𝑟 ∈ ( Base ‘ 𝑅 ) ) ) → 𝑅 ∈ Ring )
42		simprr	⊢ ( ( ( 𝐼 ∈ 𝑉 ∧ 𝑅 ∈ Ring ) ∧ ( 𝑞 ∈ ( Base ‘ 𝑅 ) ∧ 𝑟 ∈ ( Base ‘ 𝑅 ) ) ) → 𝑟 ∈ ( Base ‘ 𝑅 ) )
43	40 41 42	3jca	⊢ ( ( ( 𝐼 ∈ 𝑉 ∧ 𝑅 ∈ Ring ) ∧ ( 𝑞 ∈ ( Base ‘ 𝑅 ) ∧ 𝑟 ∈ ( Base ‘ 𝑅 ) ) ) → ( 𝐼 ∈ 𝑉 ∧ 𝑅 ∈ Ring ∧ 𝑟 ∈ ( Base ‘ 𝑅 ) ) )
44	1	lmod1lem1	⊢ ( ( 𝐼 ∈ 𝑉 ∧ 𝑅 ∈ Ring ∧ 𝑟 ∈ ( Base ‘ 𝑅 ) ) → ( 𝑟 ( ·𝑠 ‘ 𝑀 ) 𝐼 ) ∈ { 𝐼 } )
45	43 44	syl	⊢ ( ( ( 𝐼 ∈ 𝑉 ∧ 𝑅 ∈ Ring ) ∧ ( 𝑞 ∈ ( Base ‘ 𝑅 ) ∧ 𝑟 ∈ ( Base ‘ 𝑅 ) ) ) → ( 𝑟 ( ·𝑠 ‘ 𝑀 ) 𝐼 ) ∈ { 𝐼 } )
46	1	lmod1lem2	⊢ ( ( 𝐼 ∈ 𝑉 ∧ 𝑅 ∈ Ring ∧ 𝑟 ∈ ( Base ‘ 𝑅 ) ) → ( 𝑟 ( ·𝑠 ‘ 𝑀 ) ( 𝐼 ( +g ‘ 𝑀 ) 𝐼 ) ) = ( ( 𝑟 ( ·𝑠 ‘ 𝑀 ) 𝐼 ) ( +g ‘ 𝑀 ) ( 𝑟 ( ·𝑠 ‘ 𝑀 ) 𝐼 ) ) )
47	43 46	syl	⊢ ( ( ( 𝐼 ∈ 𝑉 ∧ 𝑅 ∈ Ring ) ∧ ( 𝑞 ∈ ( Base ‘ 𝑅 ) ∧ 𝑟 ∈ ( Base ‘ 𝑅 ) ) ) → ( 𝑟 ( ·𝑠 ‘ 𝑀 ) ( 𝐼 ( +g ‘ 𝑀 ) 𝐼 ) ) = ( ( 𝑟 ( ·𝑠 ‘ 𝑀 ) 𝐼 ) ( +g ‘ 𝑀 ) ( 𝑟 ( ·𝑠 ‘ 𝑀 ) 𝐼 ) ) )
48	1	lmod1lem3	⊢ ( ( ( 𝐼 ∈ 𝑉 ∧ 𝑅 ∈ Ring ) ∧ ( 𝑞 ∈ ( Base ‘ 𝑅 ) ∧ 𝑟 ∈ ( Base ‘ 𝑅 ) ) ) → ( ( 𝑞 ( +g ‘ ( Scalar ‘ 𝑀 ) ) 𝑟 ) ( ·𝑠 ‘ 𝑀 ) 𝐼 ) = ( ( 𝑞 ( ·𝑠 ‘ 𝑀 ) 𝐼 ) ( +g ‘ 𝑀 ) ( 𝑟 ( ·𝑠 ‘ 𝑀 ) 𝐼 ) ) )
49	45 47 48	3jca	⊢ ( ( ( 𝐼 ∈ 𝑉 ∧ 𝑅 ∈ Ring ) ∧ ( 𝑞 ∈ ( Base ‘ 𝑅 ) ∧ 𝑟 ∈ ( Base ‘ 𝑅 ) ) ) → ( ( 𝑟 ( ·𝑠 ‘ 𝑀 ) 𝐼 ) ∈ { 𝐼 } ∧ ( 𝑟 ( ·𝑠 ‘ 𝑀 ) ( 𝐼 ( +g ‘ 𝑀 ) 𝐼 ) ) = ( ( 𝑟 ( ·𝑠 ‘ 𝑀 ) 𝐼 ) ( +g ‘ 𝑀 ) ( 𝑟 ( ·𝑠 ‘ 𝑀 ) 𝐼 ) ) ∧ ( ( 𝑞 ( +g ‘ ( Scalar ‘ 𝑀 ) ) 𝑟 ) ( ·𝑠 ‘ 𝑀 ) 𝐼 ) = ( ( 𝑞 ( ·𝑠 ‘ 𝑀 ) 𝐼 ) ( +g ‘ 𝑀 ) ( 𝑟 ( ·𝑠 ‘ 𝑀 ) 𝐼 ) ) ) )
50	1	lmod1lem4	⊢ ( ( ( 𝐼 ∈ 𝑉 ∧ 𝑅 ∈ Ring ) ∧ ( 𝑞 ∈ ( Base ‘ 𝑅 ) ∧ 𝑟 ∈ ( Base ‘ 𝑅 ) ) ) → ( ( 𝑞 ( .r ‘ ( Scalar ‘ 𝑀 ) ) 𝑟 ) ( ·𝑠 ‘ 𝑀 ) 𝐼 ) = ( 𝑞 ( ·𝑠 ‘ 𝑀 ) ( 𝑟 ( ·𝑠 ‘ 𝑀 ) 𝐼 ) ) )
51	1	lmod1lem5	⊢ ( ( 𝐼 ∈ 𝑉 ∧ 𝑅 ∈ Ring ) → ( ( 1r ‘ ( Scalar ‘ 𝑀 ) ) ( ·𝑠 ‘ 𝑀 ) 𝐼 ) = 𝐼 )
52	51	adantr	⊢ ( ( ( 𝐼 ∈ 𝑉 ∧ 𝑅 ∈ Ring ) ∧ ( 𝑞 ∈ ( Base ‘ 𝑅 ) ∧ 𝑟 ∈ ( Base ‘ 𝑅 ) ) ) → ( ( 1r ‘ ( Scalar ‘ 𝑀 ) ) ( ·𝑠 ‘ 𝑀 ) 𝐼 ) = 𝐼 )
53	49 50 52	jca32	⊢ ( ( ( 𝐼 ∈ 𝑉 ∧ 𝑅 ∈ Ring ) ∧ ( 𝑞 ∈ ( Base ‘ 𝑅 ) ∧ 𝑟 ∈ ( Base ‘ 𝑅 ) ) ) → ( ( ( 𝑟 ( ·𝑠 ‘ 𝑀 ) 𝐼 ) ∈ { 𝐼 } ∧ ( 𝑟 ( ·𝑠 ‘ 𝑀 ) ( 𝐼 ( +g ‘ 𝑀 ) 𝐼 ) ) = ( ( 𝑟 ( ·𝑠 ‘ 𝑀 ) 𝐼 ) ( +g ‘ 𝑀 ) ( 𝑟 ( ·𝑠 ‘ 𝑀 ) 𝐼 ) ) ∧ ( ( 𝑞 ( +g ‘ ( Scalar ‘ 𝑀 ) ) 𝑟 ) ( ·𝑠 ‘ 𝑀 ) 𝐼 ) = ( ( 𝑞 ( ·𝑠 ‘ 𝑀 ) 𝐼 ) ( +g ‘ 𝑀 ) ( 𝑟 ( ·𝑠 ‘ 𝑀 ) 𝐼 ) ) ) ∧ ( ( ( 𝑞 ( .r ‘ ( Scalar ‘ 𝑀 ) ) 𝑟 ) ( ·𝑠 ‘ 𝑀 ) 𝐼 ) = ( 𝑞 ( ·𝑠 ‘ 𝑀 ) ( 𝑟 ( ·𝑠 ‘ 𝑀 ) 𝐼 ) ) ∧ ( ( 1r ‘ ( Scalar ‘ 𝑀 ) ) ( ·𝑠 ‘ 𝑀 ) 𝐼 ) = 𝐼 ) ) )
54	53	ex	⊢ ( ( 𝐼 ∈ 𝑉 ∧ 𝑅 ∈ Ring ) → ( ( 𝑞 ∈ ( Base ‘ 𝑅 ) ∧ 𝑟 ∈ ( Base ‘ 𝑅 ) ) → ( ( ( 𝑟 ( ·𝑠 ‘ 𝑀 ) 𝐼 ) ∈ { 𝐼 } ∧ ( 𝑟 ( ·𝑠 ‘ 𝑀 ) ( 𝐼 ( +g ‘ 𝑀 ) 𝐼 ) ) = ( ( 𝑟 ( ·𝑠 ‘ 𝑀 ) 𝐼 ) ( +g ‘ 𝑀 ) ( 𝑟 ( ·𝑠 ‘ 𝑀 ) 𝐼 ) ) ∧ ( ( 𝑞 ( +g ‘ ( Scalar ‘ 𝑀 ) ) 𝑟 ) ( ·𝑠 ‘ 𝑀 ) 𝐼 ) = ( ( 𝑞 ( ·𝑠 ‘ 𝑀 ) 𝐼 ) ( +g ‘ 𝑀 ) ( 𝑟 ( ·𝑠 ‘ 𝑀 ) 𝐼 ) ) ) ∧ ( ( ( 𝑞 ( .r ‘ ( Scalar ‘ 𝑀 ) ) 𝑟 ) ( ·𝑠 ‘ 𝑀 ) 𝐼 ) = ( 𝑞 ( ·𝑠 ‘ 𝑀 ) ( 𝑟 ( ·𝑠 ‘ 𝑀 ) 𝐼 ) ) ∧ ( ( 1r ‘ ( Scalar ‘ 𝑀 ) ) ( ·𝑠 ‘ 𝑀 ) 𝐼 ) = 𝐼 ) ) ) )
55	39 54	sylbid	⊢ ( ( 𝐼 ∈ 𝑉 ∧ 𝑅 ∈ Ring ) → ( ( 𝑞 ∈ ( Base ‘ ( Scalar ‘ 𝑀 ) ) ∧ 𝑟 ∈ ( Base ‘ ( Scalar ‘ 𝑀 ) ) ) → ( ( ( 𝑟 ( ·𝑠 ‘ 𝑀 ) 𝐼 ) ∈ { 𝐼 } ∧ ( 𝑟 ( ·𝑠 ‘ 𝑀 ) ( 𝐼 ( +g ‘ 𝑀 ) 𝐼 ) ) = ( ( 𝑟 ( ·𝑠 ‘ 𝑀 ) 𝐼 ) ( +g ‘ 𝑀 ) ( 𝑟 ( ·𝑠 ‘ 𝑀 ) 𝐼 ) ) ∧ ( ( 𝑞 ( +g ‘ ( Scalar ‘ 𝑀 ) ) 𝑟 ) ( ·𝑠 ‘ 𝑀 ) 𝐼 ) = ( ( 𝑞 ( ·𝑠 ‘ 𝑀 ) 𝐼 ) ( +g ‘ 𝑀 ) ( 𝑟 ( ·𝑠 ‘ 𝑀 ) 𝐼 ) ) ) ∧ ( ( ( 𝑞 ( .r ‘ ( Scalar ‘ 𝑀 ) ) 𝑟 ) ( ·𝑠 ‘ 𝑀 ) 𝐼 ) = ( 𝑞 ( ·𝑠 ‘ 𝑀 ) ( 𝑟 ( ·𝑠 ‘ 𝑀 ) 𝐼 ) ) ∧ ( ( 1r ‘ ( Scalar ‘ 𝑀 ) ) ( ·𝑠 ‘ 𝑀 ) 𝐼 ) = 𝐼 ) ) ) )
56	55	ralrimivv	⊢ ( ( 𝐼 ∈ 𝑉 ∧ 𝑅 ∈ Ring ) → ∀ 𝑞 ∈ ( Base ‘ ( Scalar ‘ 𝑀 ) ) ∀ 𝑟 ∈ ( Base ‘ ( Scalar ‘ 𝑀 ) ) ( ( ( 𝑟 ( ·𝑠 ‘ 𝑀 ) 𝐼 ) ∈ { 𝐼 } ∧ ( 𝑟 ( ·𝑠 ‘ 𝑀 ) ( 𝐼 ( +g ‘ 𝑀 ) 𝐼 ) ) = ( ( 𝑟 ( ·𝑠 ‘ 𝑀 ) 𝐼 ) ( +g ‘ 𝑀 ) ( 𝑟 ( ·𝑠 ‘ 𝑀 ) 𝐼 ) ) ∧ ( ( 𝑞 ( +g ‘ ( Scalar ‘ 𝑀 ) ) 𝑟 ) ( ·𝑠 ‘ 𝑀 ) 𝐼 ) = ( ( 𝑞 ( ·𝑠 ‘ 𝑀 ) 𝐼 ) ( +g ‘ 𝑀 ) ( 𝑟 ( ·𝑠 ‘ 𝑀 ) 𝐼 ) ) ) ∧ ( ( ( 𝑞 ( .r ‘ ( Scalar ‘ 𝑀 ) ) 𝑟 ) ( ·𝑠 ‘ 𝑀 ) 𝐼 ) = ( 𝑞 ( ·𝑠 ‘ 𝑀 ) ( 𝑟 ( ·𝑠 ‘ 𝑀 ) 𝐼 ) ) ∧ ( ( 1r ‘ ( Scalar ‘ 𝑀 ) ) ( ·𝑠 ‘ 𝑀 ) 𝐼 ) = 𝐼 ) ) )
57		oveq2	⊢ ( 𝑥 = 𝐼 → ( 𝑤 ( +g ‘ 𝑀 ) 𝑥 ) = ( 𝑤 ( +g ‘ 𝑀 ) 𝐼 ) )
58	57	oveq2d	⊢ ( 𝑥 = 𝐼 → ( 𝑟 ( ·𝑠 ‘ 𝑀 ) ( 𝑤 ( +g ‘ 𝑀 ) 𝑥 ) ) = ( 𝑟 ( ·𝑠 ‘ 𝑀 ) ( 𝑤 ( +g ‘ 𝑀 ) 𝐼 ) ) )
59		oveq2	⊢ ( 𝑥 = 𝐼 → ( 𝑟 ( ·𝑠 ‘ 𝑀 ) 𝑥 ) = ( 𝑟 ( ·𝑠 ‘ 𝑀 ) 𝐼 ) )
60	59	oveq2d	⊢ ( 𝑥 = 𝐼 → ( ( 𝑟 ( ·𝑠 ‘ 𝑀 ) 𝑤 ) ( +g ‘ 𝑀 ) ( 𝑟 ( ·𝑠 ‘ 𝑀 ) 𝑥 ) ) = ( ( 𝑟 ( ·𝑠 ‘ 𝑀 ) 𝑤 ) ( +g ‘ 𝑀 ) ( 𝑟 ( ·𝑠 ‘ 𝑀 ) 𝐼 ) ) )
61	58 60	eqeq12d	⊢ ( 𝑥 = 𝐼 → ( ( 𝑟 ( ·𝑠 ‘ 𝑀 ) ( 𝑤 ( +g ‘ 𝑀 ) 𝑥 ) ) = ( ( 𝑟 ( ·𝑠 ‘ 𝑀 ) 𝑤 ) ( +g ‘ 𝑀 ) ( 𝑟 ( ·𝑠 ‘ 𝑀 ) 𝑥 ) ) ↔ ( 𝑟 ( ·𝑠 ‘ 𝑀 ) ( 𝑤 ( +g ‘ 𝑀 ) 𝐼 ) ) = ( ( 𝑟 ( ·𝑠 ‘ 𝑀 ) 𝑤 ) ( +g ‘ 𝑀 ) ( 𝑟 ( ·𝑠 ‘ 𝑀 ) 𝐼 ) ) ) )
62	61	3anbi2d	⊢ ( 𝑥 = 𝐼 → ( ( ( 𝑟 ( ·𝑠 ‘ 𝑀 ) 𝑤 ) ∈ { 𝐼 } ∧ ( 𝑟 ( ·𝑠 ‘ 𝑀 ) ( 𝑤 ( +g ‘ 𝑀 ) 𝑥 ) ) = ( ( 𝑟 ( ·𝑠 ‘ 𝑀 ) 𝑤 ) ( +g ‘ 𝑀 ) ( 𝑟 ( ·𝑠 ‘ 𝑀 ) 𝑥 ) ) ∧ ( ( 𝑞 ( +g ‘ ( Scalar ‘ 𝑀 ) ) 𝑟 ) ( ·𝑠 ‘ 𝑀 ) 𝑤 ) = ( ( 𝑞 ( ·𝑠 ‘ 𝑀 ) 𝑤 ) ( +g ‘ 𝑀 ) ( 𝑟 ( ·𝑠 ‘ 𝑀 ) 𝑤 ) ) ) ↔ ( ( 𝑟 ( ·𝑠 ‘ 𝑀 ) 𝑤 ) ∈ { 𝐼 } ∧ ( 𝑟 ( ·𝑠 ‘ 𝑀 ) ( 𝑤 ( +g ‘ 𝑀 ) 𝐼 ) ) = ( ( 𝑟 ( ·𝑠 ‘ 𝑀 ) 𝑤 ) ( +g ‘ 𝑀 ) ( 𝑟 ( ·𝑠 ‘ 𝑀 ) 𝐼 ) ) ∧ ( ( 𝑞 ( +g ‘ ( Scalar ‘ 𝑀 ) ) 𝑟 ) ( ·𝑠 ‘ 𝑀 ) 𝑤 ) = ( ( 𝑞 ( ·𝑠 ‘ 𝑀 ) 𝑤 ) ( +g ‘ 𝑀 ) ( 𝑟 ( ·𝑠 ‘ 𝑀 ) 𝑤 ) ) ) ) )
63	62	anbi1d	⊢ ( 𝑥 = 𝐼 → ( ( ( ( 𝑟 ( ·𝑠 ‘ 𝑀 ) 𝑤 ) ∈ { 𝐼 } ∧ ( 𝑟 ( ·𝑠 ‘ 𝑀 ) ( 𝑤 ( +g ‘ 𝑀 ) 𝑥 ) ) = ( ( 𝑟 ( ·𝑠 ‘ 𝑀 ) 𝑤 ) ( +g ‘ 𝑀 ) ( 𝑟 ( ·𝑠 ‘ 𝑀 ) 𝑥 ) ) ∧ ( ( 𝑞 ( +g ‘ ( Scalar ‘ 𝑀 ) ) 𝑟 ) ( ·𝑠 ‘ 𝑀 ) 𝑤 ) = ( ( 𝑞 ( ·𝑠 ‘ 𝑀 ) 𝑤 ) ( +g ‘ 𝑀 ) ( 𝑟 ( ·𝑠 ‘ 𝑀 ) 𝑤 ) ) ) ∧ ( ( ( 𝑞 ( .r ‘ ( Scalar ‘ 𝑀 ) ) 𝑟 ) ( ·𝑠 ‘ 𝑀 ) 𝑤 ) = ( 𝑞 ( ·𝑠 ‘ 𝑀 ) ( 𝑟 ( ·𝑠 ‘ 𝑀 ) 𝑤 ) ) ∧ ( ( 1r ‘ ( Scalar ‘ 𝑀 ) ) ( ·𝑠 ‘ 𝑀 ) 𝑤 ) = 𝑤 ) ) ↔ ( ( ( 𝑟 ( ·𝑠 ‘ 𝑀 ) 𝑤 ) ∈ { 𝐼 } ∧ ( 𝑟 ( ·𝑠 ‘ 𝑀 ) ( 𝑤 ( +g ‘ 𝑀 ) 𝐼 ) ) = ( ( 𝑟 ( ·𝑠 ‘ 𝑀 ) 𝑤 ) ( +g ‘ 𝑀 ) ( 𝑟 ( ·𝑠 ‘ 𝑀 ) 𝐼 ) ) ∧ ( ( 𝑞 ( +g ‘ ( Scalar ‘ 𝑀 ) ) 𝑟 ) ( ·𝑠 ‘ 𝑀 ) 𝑤 ) = ( ( 𝑞 ( ·𝑠 ‘ 𝑀 ) 𝑤 ) ( +g ‘ 𝑀 ) ( 𝑟 ( ·𝑠 ‘ 𝑀 ) 𝑤 ) ) ) ∧ ( ( ( 𝑞 ( .r ‘ ( Scalar ‘ 𝑀 ) ) 𝑟 ) ( ·𝑠 ‘ 𝑀 ) 𝑤 ) = ( 𝑞 ( ·𝑠 ‘ 𝑀 ) ( 𝑟 ( ·𝑠 ‘ 𝑀 ) 𝑤 ) ) ∧ ( ( 1r ‘ ( Scalar ‘ 𝑀 ) ) ( ·𝑠 ‘ 𝑀 ) 𝑤 ) = 𝑤 ) ) ) )
64	63	ralbidv	⊢ ( 𝑥 = 𝐼 → ( ∀ 𝑤 ∈ { 𝐼 } ( ( ( 𝑟 ( ·𝑠 ‘ 𝑀 ) 𝑤 ) ∈ { 𝐼 } ∧ ( 𝑟 ( ·𝑠 ‘ 𝑀 ) ( 𝑤 ( +g ‘ 𝑀 ) 𝑥 ) ) = ( ( 𝑟 ( ·𝑠 ‘ 𝑀 ) 𝑤 ) ( +g ‘ 𝑀 ) ( 𝑟 ( ·𝑠 ‘ 𝑀 ) 𝑥 ) ) ∧ ( ( 𝑞 ( +g ‘ ( Scalar ‘ 𝑀 ) ) 𝑟 ) ( ·𝑠 ‘ 𝑀 ) 𝑤 ) = ( ( 𝑞 ( ·𝑠 ‘ 𝑀 ) 𝑤 ) ( +g ‘ 𝑀 ) ( 𝑟 ( ·𝑠 ‘ 𝑀 ) 𝑤 ) ) ) ∧ ( ( ( 𝑞 ( .r ‘ ( Scalar ‘ 𝑀 ) ) 𝑟 ) ( ·𝑠 ‘ 𝑀 ) 𝑤 ) = ( 𝑞 ( ·𝑠 ‘ 𝑀 ) ( 𝑟 ( ·𝑠 ‘ 𝑀 ) 𝑤 ) ) ∧ ( ( 1r ‘ ( Scalar ‘ 𝑀 ) ) ( ·𝑠 ‘ 𝑀 ) 𝑤 ) = 𝑤 ) ) ↔ ∀ 𝑤 ∈ { 𝐼 } ( ( ( 𝑟 ( ·𝑠 ‘ 𝑀 ) 𝑤 ) ∈ { 𝐼 } ∧ ( 𝑟 ( ·𝑠 ‘ 𝑀 ) ( 𝑤 ( +g ‘ 𝑀 ) 𝐼 ) ) = ( ( 𝑟 ( ·𝑠 ‘ 𝑀 ) 𝑤 ) ( +g ‘ 𝑀 ) ( 𝑟 ( ·𝑠 ‘ 𝑀 ) 𝐼 ) ) ∧ ( ( 𝑞 ( +g ‘ ( Scalar ‘ 𝑀 ) ) 𝑟 ) ( ·𝑠 ‘ 𝑀 ) 𝑤 ) = ( ( 𝑞 ( ·𝑠 ‘ 𝑀 ) 𝑤 ) ( +g ‘ 𝑀 ) ( 𝑟 ( ·𝑠 ‘ 𝑀 ) 𝑤 ) ) ) ∧ ( ( ( 𝑞 ( .r ‘ ( Scalar ‘ 𝑀 ) ) 𝑟 ) ( ·𝑠 ‘ 𝑀 ) 𝑤 ) = ( 𝑞 ( ·𝑠 ‘ 𝑀 ) ( 𝑟 ( ·𝑠 ‘ 𝑀 ) 𝑤 ) ) ∧ ( ( 1r ‘ ( Scalar ‘ 𝑀 ) ) ( ·𝑠 ‘ 𝑀 ) 𝑤 ) = 𝑤 ) ) ) )
65	64	ralsng	⊢ ( 𝐼 ∈ 𝑉 → ( ∀ 𝑥 ∈ { 𝐼 } ∀ 𝑤 ∈ { 𝐼 } ( ( ( 𝑟 ( ·𝑠 ‘ 𝑀 ) 𝑤 ) ∈ { 𝐼 } ∧ ( 𝑟 ( ·𝑠 ‘ 𝑀 ) ( 𝑤 ( +g ‘ 𝑀 ) 𝑥 ) ) = ( ( 𝑟 ( ·𝑠 ‘ 𝑀 ) 𝑤 ) ( +g ‘ 𝑀 ) ( 𝑟 ( ·𝑠 ‘ 𝑀 ) 𝑥 ) ) ∧ ( ( 𝑞 ( +g ‘ ( Scalar ‘ 𝑀 ) ) 𝑟 ) ( ·𝑠 ‘ 𝑀 ) 𝑤 ) = ( ( 𝑞 ( ·𝑠 ‘ 𝑀 ) 𝑤 ) ( +g ‘ 𝑀 ) ( 𝑟 ( ·𝑠 ‘ 𝑀 ) 𝑤 ) ) ) ∧ ( ( ( 𝑞 ( .r ‘ ( Scalar ‘ 𝑀 ) ) 𝑟 ) ( ·𝑠 ‘ 𝑀 ) 𝑤 ) = ( 𝑞 ( ·𝑠 ‘ 𝑀 ) ( 𝑟 ( ·𝑠 ‘ 𝑀 ) 𝑤 ) ) ∧ ( ( 1r ‘ ( Scalar ‘ 𝑀 ) ) ( ·𝑠 ‘ 𝑀 ) 𝑤 ) = 𝑤 ) ) ↔ ∀ 𝑤 ∈ { 𝐼 } ( ( ( 𝑟 ( ·𝑠 ‘ 𝑀 ) 𝑤 ) ∈ { 𝐼 } ∧ ( 𝑟 ( ·𝑠 ‘ 𝑀 ) ( 𝑤 ( +g ‘ 𝑀 ) 𝐼 ) ) = ( ( 𝑟 ( ·𝑠 ‘ 𝑀 ) 𝑤 ) ( +g ‘ 𝑀 ) ( 𝑟 ( ·𝑠 ‘ 𝑀 ) 𝐼 ) ) ∧ ( ( 𝑞 ( +g ‘ ( Scalar ‘ 𝑀 ) ) 𝑟 ) ( ·𝑠 ‘ 𝑀 ) 𝑤 ) = ( ( 𝑞 ( ·𝑠 ‘ 𝑀 ) 𝑤 ) ( +g ‘ 𝑀 ) ( 𝑟 ( ·𝑠 ‘ 𝑀 ) 𝑤 ) ) ) ∧ ( ( ( 𝑞 ( .r ‘ ( Scalar ‘ 𝑀 ) ) 𝑟 ) ( ·𝑠 ‘ 𝑀 ) 𝑤 ) = ( 𝑞 ( ·𝑠 ‘ 𝑀 ) ( 𝑟 ( ·𝑠 ‘ 𝑀 ) 𝑤 ) ) ∧ ( ( 1r ‘ ( Scalar ‘ 𝑀 ) ) ( ·𝑠 ‘ 𝑀 ) 𝑤 ) = 𝑤 ) ) ) )
66	65	adantr	⊢ ( ( 𝐼 ∈ 𝑉 ∧ 𝑅 ∈ Ring ) → ( ∀ 𝑥 ∈ { 𝐼 } ∀ 𝑤 ∈ { 𝐼 } ( ( ( 𝑟 ( ·𝑠 ‘ 𝑀 ) 𝑤 ) ∈ { 𝐼 } ∧ ( 𝑟 ( ·𝑠 ‘ 𝑀 ) ( 𝑤 ( +g ‘ 𝑀 ) 𝑥 ) ) = ( ( 𝑟 ( ·𝑠 ‘ 𝑀 ) 𝑤 ) ( +g ‘ 𝑀 ) ( 𝑟 ( ·𝑠 ‘ 𝑀 ) 𝑥 ) ) ∧ ( ( 𝑞 ( +g ‘ ( Scalar ‘ 𝑀 ) ) 𝑟 ) ( ·𝑠 ‘ 𝑀 ) 𝑤 ) = ( ( 𝑞 ( ·𝑠 ‘ 𝑀 ) 𝑤 ) ( +g ‘ 𝑀 ) ( 𝑟 ( ·𝑠 ‘ 𝑀 ) 𝑤 ) ) ) ∧ ( ( ( 𝑞 ( .r ‘ ( Scalar ‘ 𝑀 ) ) 𝑟 ) ( ·𝑠 ‘ 𝑀 ) 𝑤 ) = ( 𝑞 ( ·𝑠 ‘ 𝑀 ) ( 𝑟 ( ·𝑠 ‘ 𝑀 ) 𝑤 ) ) ∧ ( ( 1r ‘ ( Scalar ‘ 𝑀 ) ) ( ·𝑠 ‘ 𝑀 ) 𝑤 ) = 𝑤 ) ) ↔ ∀ 𝑤 ∈ { 𝐼 } ( ( ( 𝑟 ( ·𝑠 ‘ 𝑀 ) 𝑤 ) ∈ { 𝐼 } ∧ ( 𝑟 ( ·𝑠 ‘ 𝑀 ) ( 𝑤 ( +g ‘ 𝑀 ) 𝐼 ) ) = ( ( 𝑟 ( ·𝑠 ‘ 𝑀 ) 𝑤 ) ( +g ‘ 𝑀 ) ( 𝑟 ( ·𝑠 ‘ 𝑀 ) 𝐼 ) ) ∧ ( ( 𝑞 ( +g ‘ ( Scalar ‘ 𝑀 ) ) 𝑟 ) ( ·𝑠 ‘ 𝑀 ) 𝑤 ) = ( ( 𝑞 ( ·𝑠 ‘ 𝑀 ) 𝑤 ) ( +g ‘ 𝑀 ) ( 𝑟 ( ·𝑠 ‘ 𝑀 ) 𝑤 ) ) ) ∧ ( ( ( 𝑞 ( .r ‘ ( Scalar ‘ 𝑀 ) ) 𝑟 ) ( ·𝑠 ‘ 𝑀 ) 𝑤 ) = ( 𝑞 ( ·𝑠 ‘ 𝑀 ) ( 𝑟 ( ·𝑠 ‘ 𝑀 ) 𝑤 ) ) ∧ ( ( 1r ‘ ( Scalar ‘ 𝑀 ) ) ( ·𝑠 ‘ 𝑀 ) 𝑤 ) = 𝑤 ) ) ) )
67		oveq2	⊢ ( 𝑤 = 𝐼 → ( 𝑟 ( ·𝑠 ‘ 𝑀 ) 𝑤 ) = ( 𝑟 ( ·𝑠 ‘ 𝑀 ) 𝐼 ) )
68	67	eleq1d	⊢ ( 𝑤 = 𝐼 → ( ( 𝑟 ( ·𝑠 ‘ 𝑀 ) 𝑤 ) ∈ { 𝐼 } ↔ ( 𝑟 ( ·𝑠 ‘ 𝑀 ) 𝐼 ) ∈ { 𝐼 } ) )
69		oveq1	⊢ ( 𝑤 = 𝐼 → ( 𝑤 ( +g ‘ 𝑀 ) 𝐼 ) = ( 𝐼 ( +g ‘ 𝑀 ) 𝐼 ) )
70	69	oveq2d	⊢ ( 𝑤 = 𝐼 → ( 𝑟 ( ·𝑠 ‘ 𝑀 ) ( 𝑤 ( +g ‘ 𝑀 ) 𝐼 ) ) = ( 𝑟 ( ·𝑠 ‘ 𝑀 ) ( 𝐼 ( +g ‘ 𝑀 ) 𝐼 ) ) )
71	67	oveq1d	⊢ ( 𝑤 = 𝐼 → ( ( 𝑟 ( ·𝑠 ‘ 𝑀 ) 𝑤 ) ( +g ‘ 𝑀 ) ( 𝑟 ( ·𝑠 ‘ 𝑀 ) 𝐼 ) ) = ( ( 𝑟 ( ·𝑠 ‘ 𝑀 ) 𝐼 ) ( +g ‘ 𝑀 ) ( 𝑟 ( ·𝑠 ‘ 𝑀 ) 𝐼 ) ) )
72	70 71	eqeq12d	⊢ ( 𝑤 = 𝐼 → ( ( 𝑟 ( ·𝑠 ‘ 𝑀 ) ( 𝑤 ( +g ‘ 𝑀 ) 𝐼 ) ) = ( ( 𝑟 ( ·𝑠 ‘ 𝑀 ) 𝑤 ) ( +g ‘ 𝑀 ) ( 𝑟 ( ·𝑠 ‘ 𝑀 ) 𝐼 ) ) ↔ ( 𝑟 ( ·𝑠 ‘ 𝑀 ) ( 𝐼 ( +g ‘ 𝑀 ) 𝐼 ) ) = ( ( 𝑟 ( ·𝑠 ‘ 𝑀 ) 𝐼 ) ( +g ‘ 𝑀 ) ( 𝑟 ( ·𝑠 ‘ 𝑀 ) 𝐼 ) ) ) )
73		oveq2	⊢ ( 𝑤 = 𝐼 → ( ( 𝑞 ( +g ‘ ( Scalar ‘ 𝑀 ) ) 𝑟 ) ( ·𝑠 ‘ 𝑀 ) 𝑤 ) = ( ( 𝑞 ( +g ‘ ( Scalar ‘ 𝑀 ) ) 𝑟 ) ( ·𝑠 ‘ 𝑀 ) 𝐼 ) )
74		oveq2	⊢ ( 𝑤 = 𝐼 → ( 𝑞 ( ·𝑠 ‘ 𝑀 ) 𝑤 ) = ( 𝑞 ( ·𝑠 ‘ 𝑀 ) 𝐼 ) )
75	74 67	oveq12d	⊢ ( 𝑤 = 𝐼 → ( ( 𝑞 ( ·𝑠 ‘ 𝑀 ) 𝑤 ) ( +g ‘ 𝑀 ) ( 𝑟 ( ·𝑠 ‘ 𝑀 ) 𝑤 ) ) = ( ( 𝑞 ( ·𝑠 ‘ 𝑀 ) 𝐼 ) ( +g ‘ 𝑀 ) ( 𝑟 ( ·𝑠 ‘ 𝑀 ) 𝐼 ) ) )
76	73 75	eqeq12d	⊢ ( 𝑤 = 𝐼 → ( ( ( 𝑞 ( +g ‘ ( Scalar ‘ 𝑀 ) ) 𝑟 ) ( ·𝑠 ‘ 𝑀 ) 𝑤 ) = ( ( 𝑞 ( ·𝑠 ‘ 𝑀 ) 𝑤 ) ( +g ‘ 𝑀 ) ( 𝑟 ( ·𝑠 ‘ 𝑀 ) 𝑤 ) ) ↔ ( ( 𝑞 ( +g ‘ ( Scalar ‘ 𝑀 ) ) 𝑟 ) ( ·𝑠 ‘ 𝑀 ) 𝐼 ) = ( ( 𝑞 ( ·𝑠 ‘ 𝑀 ) 𝐼 ) ( +g ‘ 𝑀 ) ( 𝑟 ( ·𝑠 ‘ 𝑀 ) 𝐼 ) ) ) )
77	68 72 76	3anbi123d	⊢ ( 𝑤 = 𝐼 → ( ( ( 𝑟 ( ·𝑠 ‘ 𝑀 ) 𝑤 ) ∈ { 𝐼 } ∧ ( 𝑟 ( ·𝑠 ‘ 𝑀 ) ( 𝑤 ( +g ‘ 𝑀 ) 𝐼 ) ) = ( ( 𝑟 ( ·𝑠 ‘ 𝑀 ) 𝑤 ) ( +g ‘ 𝑀 ) ( 𝑟 ( ·𝑠 ‘ 𝑀 ) 𝐼 ) ) ∧ ( ( 𝑞 ( +g ‘ ( Scalar ‘ 𝑀 ) ) 𝑟 ) ( ·𝑠 ‘ 𝑀 ) 𝑤 ) = ( ( 𝑞 ( ·𝑠 ‘ 𝑀 ) 𝑤 ) ( +g ‘ 𝑀 ) ( 𝑟 ( ·𝑠 ‘ 𝑀 ) 𝑤 ) ) ) ↔ ( ( 𝑟 ( ·𝑠 ‘ 𝑀 ) 𝐼 ) ∈ { 𝐼 } ∧ ( 𝑟 ( ·𝑠 ‘ 𝑀 ) ( 𝐼 ( +g ‘ 𝑀 ) 𝐼 ) ) = ( ( 𝑟 ( ·𝑠 ‘ 𝑀 ) 𝐼 ) ( +g ‘ 𝑀 ) ( 𝑟 ( ·𝑠 ‘ 𝑀 ) 𝐼 ) ) ∧ ( ( 𝑞 ( +g ‘ ( Scalar ‘ 𝑀 ) ) 𝑟 ) ( ·𝑠 ‘ 𝑀 ) 𝐼 ) = ( ( 𝑞 ( ·𝑠 ‘ 𝑀 ) 𝐼 ) ( +g ‘ 𝑀 ) ( 𝑟 ( ·𝑠 ‘ 𝑀 ) 𝐼 ) ) ) ) )
78		oveq2	⊢ ( 𝑤 = 𝐼 → ( ( 𝑞 ( .r ‘ ( Scalar ‘ 𝑀 ) ) 𝑟 ) ( ·𝑠 ‘ 𝑀 ) 𝑤 ) = ( ( 𝑞 ( .r ‘ ( Scalar ‘ 𝑀 ) ) 𝑟 ) ( ·𝑠 ‘ 𝑀 ) 𝐼 ) )
79	67	oveq2d	⊢ ( 𝑤 = 𝐼 → ( 𝑞 ( ·𝑠 ‘ 𝑀 ) ( 𝑟 ( ·𝑠 ‘ 𝑀 ) 𝑤 ) ) = ( 𝑞 ( ·𝑠 ‘ 𝑀 ) ( 𝑟 ( ·𝑠 ‘ 𝑀 ) 𝐼 ) ) )
80	78 79	eqeq12d	⊢ ( 𝑤 = 𝐼 → ( ( ( 𝑞 ( .r ‘ ( Scalar ‘ 𝑀 ) ) 𝑟 ) ( ·𝑠 ‘ 𝑀 ) 𝑤 ) = ( 𝑞 ( ·𝑠 ‘ 𝑀 ) ( 𝑟 ( ·𝑠 ‘ 𝑀 ) 𝑤 ) ) ↔ ( ( 𝑞 ( .r ‘ ( Scalar ‘ 𝑀 ) ) 𝑟 ) ( ·𝑠 ‘ 𝑀 ) 𝐼 ) = ( 𝑞 ( ·𝑠 ‘ 𝑀 ) ( 𝑟 ( ·𝑠 ‘ 𝑀 ) 𝐼 ) ) ) )
81		oveq2	⊢ ( 𝑤 = 𝐼 → ( ( 1r ‘ ( Scalar ‘ 𝑀 ) ) ( ·𝑠 ‘ 𝑀 ) 𝑤 ) = ( ( 1r ‘ ( Scalar ‘ 𝑀 ) ) ( ·𝑠 ‘ 𝑀 ) 𝐼 ) )
82		id	⊢ ( 𝑤 = 𝐼 → 𝑤 = 𝐼 )
83	81 82	eqeq12d	⊢ ( 𝑤 = 𝐼 → ( ( ( 1r ‘ ( Scalar ‘ 𝑀 ) ) ( ·𝑠 ‘ 𝑀 ) 𝑤 ) = 𝑤 ↔ ( ( 1r ‘ ( Scalar ‘ 𝑀 ) ) ( ·𝑠 ‘ 𝑀 ) 𝐼 ) = 𝐼 ) )
84	80 83	anbi12d	⊢ ( 𝑤 = 𝐼 → ( ( ( ( 𝑞 ( .r ‘ ( Scalar ‘ 𝑀 ) ) 𝑟 ) ( ·𝑠 ‘ 𝑀 ) 𝑤 ) = ( 𝑞 ( ·𝑠 ‘ 𝑀 ) ( 𝑟 ( ·𝑠 ‘ 𝑀 ) 𝑤 ) ) ∧ ( ( 1r ‘ ( Scalar ‘ 𝑀 ) ) ( ·𝑠 ‘ 𝑀 ) 𝑤 ) = 𝑤 ) ↔ ( ( ( 𝑞 ( .r ‘ ( Scalar ‘ 𝑀 ) ) 𝑟 ) ( ·𝑠 ‘ 𝑀 ) 𝐼 ) = ( 𝑞 ( ·𝑠 ‘ 𝑀 ) ( 𝑟 ( ·𝑠 ‘ 𝑀 ) 𝐼 ) ) ∧ ( ( 1r ‘ ( Scalar ‘ 𝑀 ) ) ( ·𝑠 ‘ 𝑀 ) 𝐼 ) = 𝐼 ) ) )
85	77 84	anbi12d	⊢ ( 𝑤 = 𝐼 → ( ( ( ( 𝑟 ( ·𝑠 ‘ 𝑀 ) 𝑤 ) ∈ { 𝐼 } ∧ ( 𝑟 ( ·𝑠 ‘ 𝑀 ) ( 𝑤 ( +g ‘ 𝑀 ) 𝐼 ) ) = ( ( 𝑟 ( ·𝑠 ‘ 𝑀 ) 𝑤 ) ( +g ‘ 𝑀 ) ( 𝑟 ( ·𝑠 ‘ 𝑀 ) 𝐼 ) ) ∧ ( ( 𝑞 ( +g ‘ ( Scalar ‘ 𝑀 ) ) 𝑟 ) ( ·𝑠 ‘ 𝑀 ) 𝑤 ) = ( ( 𝑞 ( ·𝑠 ‘ 𝑀 ) 𝑤 ) ( +g ‘ 𝑀 ) ( 𝑟 ( ·𝑠 ‘ 𝑀 ) 𝑤 ) ) ) ∧ ( ( ( 𝑞 ( .r ‘ ( Scalar ‘ 𝑀 ) ) 𝑟 ) ( ·𝑠 ‘ 𝑀 ) 𝑤 ) = ( 𝑞 ( ·𝑠 ‘ 𝑀 ) ( 𝑟 ( ·𝑠 ‘ 𝑀 ) 𝑤 ) ) ∧ ( ( 1r ‘ ( Scalar ‘ 𝑀 ) ) ( ·𝑠 ‘ 𝑀 ) 𝑤 ) = 𝑤 ) ) ↔ ( ( ( 𝑟 ( ·𝑠 ‘ 𝑀 ) 𝐼 ) ∈ { 𝐼 } ∧ ( 𝑟 ( ·𝑠 ‘ 𝑀 ) ( 𝐼 ( +g ‘ 𝑀 ) 𝐼 ) ) = ( ( 𝑟 ( ·𝑠 ‘ 𝑀 ) 𝐼 ) ( +g ‘ 𝑀 ) ( 𝑟 ( ·𝑠 ‘ 𝑀 ) 𝐼 ) ) ∧ ( ( 𝑞 ( +g ‘ ( Scalar ‘ 𝑀 ) ) 𝑟 ) ( ·𝑠 ‘ 𝑀 ) 𝐼 ) = ( ( 𝑞 ( ·𝑠 ‘ 𝑀 ) 𝐼 ) ( +g ‘ 𝑀 ) ( 𝑟 ( ·𝑠 ‘ 𝑀 ) 𝐼 ) ) ) ∧ ( ( ( 𝑞 ( .r ‘ ( Scalar ‘ 𝑀 ) ) 𝑟 ) ( ·𝑠 ‘ 𝑀 ) 𝐼 ) = ( 𝑞 ( ·𝑠 ‘ 𝑀 ) ( 𝑟 ( ·𝑠 ‘ 𝑀 ) 𝐼 ) ) ∧ ( ( 1r ‘ ( Scalar ‘ 𝑀 ) ) ( ·𝑠 ‘ 𝑀 ) 𝐼 ) = 𝐼 ) ) ) )
86	85	ralsng	⊢ ( 𝐼 ∈ 𝑉 → ( ∀ 𝑤 ∈ { 𝐼 } ( ( ( 𝑟 ( ·𝑠 ‘ 𝑀 ) 𝑤 ) ∈ { 𝐼 } ∧ ( 𝑟 ( ·𝑠 ‘ 𝑀 ) ( 𝑤 ( +g ‘ 𝑀 ) 𝐼 ) ) = ( ( 𝑟 ( ·𝑠 ‘ 𝑀 ) 𝑤 ) ( +g ‘ 𝑀 ) ( 𝑟 ( ·𝑠 ‘ 𝑀 ) 𝐼 ) ) ∧ ( ( 𝑞 ( +g ‘ ( Scalar ‘ 𝑀 ) ) 𝑟 ) ( ·𝑠 ‘ 𝑀 ) 𝑤 ) = ( ( 𝑞 ( ·𝑠 ‘ 𝑀 ) 𝑤 ) ( +g ‘ 𝑀 ) ( 𝑟 ( ·𝑠 ‘ 𝑀 ) 𝑤 ) ) ) ∧ ( ( ( 𝑞 ( .r ‘ ( Scalar ‘ 𝑀 ) ) 𝑟 ) ( ·𝑠 ‘ 𝑀 ) 𝑤 ) = ( 𝑞 ( ·𝑠 ‘ 𝑀 ) ( 𝑟 ( ·𝑠 ‘ 𝑀 ) 𝑤 ) ) ∧ ( ( 1r ‘ ( Scalar ‘ 𝑀 ) ) ( ·𝑠 ‘ 𝑀 ) 𝑤 ) = 𝑤 ) ) ↔ ( ( ( 𝑟 ( ·𝑠 ‘ 𝑀 ) 𝐼 ) ∈ { 𝐼 } ∧ ( 𝑟 ( ·𝑠 ‘ 𝑀 ) ( 𝐼 ( +g ‘ 𝑀 ) 𝐼 ) ) = ( ( 𝑟 ( ·𝑠 ‘ 𝑀 ) 𝐼 ) ( +g ‘ 𝑀 ) ( 𝑟 ( ·𝑠 ‘ 𝑀 ) 𝐼 ) ) ∧ ( ( 𝑞 ( +g ‘ ( Scalar ‘ 𝑀 ) ) 𝑟 ) ( ·𝑠 ‘ 𝑀 ) 𝐼 ) = ( ( 𝑞 ( ·𝑠 ‘ 𝑀 ) 𝐼 ) ( +g ‘ 𝑀 ) ( 𝑟 ( ·𝑠 ‘ 𝑀 ) 𝐼 ) ) ) ∧ ( ( ( 𝑞 ( .r ‘ ( Scalar ‘ 𝑀 ) ) 𝑟 ) ( ·𝑠 ‘ 𝑀 ) 𝐼 ) = ( 𝑞 ( ·𝑠 ‘ 𝑀 ) ( 𝑟 ( ·𝑠 ‘ 𝑀 ) 𝐼 ) ) ∧ ( ( 1r ‘ ( Scalar ‘ 𝑀 ) ) ( ·𝑠 ‘ 𝑀 ) 𝐼 ) = 𝐼 ) ) ) )
87	86	adantr	⊢ ( ( 𝐼 ∈ 𝑉 ∧ 𝑅 ∈ Ring ) → ( ∀ 𝑤 ∈ { 𝐼 } ( ( ( 𝑟 ( ·𝑠 ‘ 𝑀 ) 𝑤 ) ∈ { 𝐼 } ∧ ( 𝑟 ( ·𝑠 ‘ 𝑀 ) ( 𝑤 ( +g ‘ 𝑀 ) 𝐼 ) ) = ( ( 𝑟 ( ·𝑠 ‘ 𝑀 ) 𝑤 ) ( +g ‘ 𝑀 ) ( 𝑟 ( ·𝑠 ‘ 𝑀 ) 𝐼 ) ) ∧ ( ( 𝑞 ( +g ‘ ( Scalar ‘ 𝑀 ) ) 𝑟 ) ( ·𝑠 ‘ 𝑀 ) 𝑤 ) = ( ( 𝑞 ( ·𝑠 ‘ 𝑀 ) 𝑤 ) ( +g ‘ 𝑀 ) ( 𝑟 ( ·𝑠 ‘ 𝑀 ) 𝑤 ) ) ) ∧ ( ( ( 𝑞 ( .r ‘ ( Scalar ‘ 𝑀 ) ) 𝑟 ) ( ·𝑠 ‘ 𝑀 ) 𝑤 ) = ( 𝑞 ( ·𝑠 ‘ 𝑀 ) ( 𝑟 ( ·𝑠 ‘ 𝑀 ) 𝑤 ) ) ∧ ( ( 1r ‘ ( Scalar ‘ 𝑀 ) ) ( ·𝑠 ‘ 𝑀 ) 𝑤 ) = 𝑤 ) ) ↔ ( ( ( 𝑟 ( ·𝑠 ‘ 𝑀 ) 𝐼 ) ∈ { 𝐼 } ∧ ( 𝑟 ( ·𝑠 ‘ 𝑀 ) ( 𝐼 ( +g ‘ 𝑀 ) 𝐼 ) ) = ( ( 𝑟 ( ·𝑠 ‘ 𝑀 ) 𝐼 ) ( +g ‘ 𝑀 ) ( 𝑟 ( ·𝑠 ‘ 𝑀 ) 𝐼 ) ) ∧ ( ( 𝑞 ( +g ‘ ( Scalar ‘ 𝑀 ) ) 𝑟 ) ( ·𝑠 ‘ 𝑀 ) 𝐼 ) = ( ( 𝑞 ( ·𝑠 ‘ 𝑀 ) 𝐼 ) ( +g ‘ 𝑀 ) ( 𝑟 ( ·𝑠 ‘ 𝑀 ) 𝐼 ) ) ) ∧ ( ( ( 𝑞 ( .r ‘ ( Scalar ‘ 𝑀 ) ) 𝑟 ) ( ·𝑠 ‘ 𝑀 ) 𝐼 ) = ( 𝑞 ( ·𝑠 ‘ 𝑀 ) ( 𝑟 ( ·𝑠 ‘ 𝑀 ) 𝐼 ) ) ∧ ( ( 1r ‘ ( Scalar ‘ 𝑀 ) ) ( ·𝑠 ‘ 𝑀 ) 𝐼 ) = 𝐼 ) ) ) )
88	66 87	bitrd	⊢ ( ( 𝐼 ∈ 𝑉 ∧ 𝑅 ∈ Ring ) → ( ∀ 𝑥 ∈ { 𝐼 } ∀ 𝑤 ∈ { 𝐼 } ( ( ( 𝑟 ( ·𝑠 ‘ 𝑀 ) 𝑤 ) ∈ { 𝐼 } ∧ ( 𝑟 ( ·𝑠 ‘ 𝑀 ) ( 𝑤 ( +g ‘ 𝑀 ) 𝑥 ) ) = ( ( 𝑟 ( ·𝑠 ‘ 𝑀 ) 𝑤 ) ( +g ‘ 𝑀 ) ( 𝑟 ( ·𝑠 ‘ 𝑀 ) 𝑥 ) ) ∧ ( ( 𝑞 ( +g ‘ ( Scalar ‘ 𝑀 ) ) 𝑟 ) ( ·𝑠 ‘ 𝑀 ) 𝑤 ) = ( ( 𝑞 ( ·𝑠 ‘ 𝑀 ) 𝑤 ) ( +g ‘ 𝑀 ) ( 𝑟 ( ·𝑠 ‘ 𝑀 ) 𝑤 ) ) ) ∧ ( ( ( 𝑞 ( .r ‘ ( Scalar ‘ 𝑀 ) ) 𝑟 ) ( ·𝑠 ‘ 𝑀 ) 𝑤 ) = ( 𝑞 ( ·𝑠 ‘ 𝑀 ) ( 𝑟 ( ·𝑠 ‘ 𝑀 ) 𝑤 ) ) ∧ ( ( 1r ‘ ( Scalar ‘ 𝑀 ) ) ( ·𝑠 ‘ 𝑀 ) 𝑤 ) = 𝑤 ) ) ↔ ( ( ( 𝑟 ( ·𝑠 ‘ 𝑀 ) 𝐼 ) ∈ { 𝐼 } ∧ ( 𝑟 ( ·𝑠 ‘ 𝑀 ) ( 𝐼 ( +g ‘ 𝑀 ) 𝐼 ) ) = ( ( 𝑟 ( ·𝑠 ‘ 𝑀 ) 𝐼 ) ( +g ‘ 𝑀 ) ( 𝑟 ( ·𝑠 ‘ 𝑀 ) 𝐼 ) ) ∧ ( ( 𝑞 ( +g ‘ ( Scalar ‘ 𝑀 ) ) 𝑟 ) ( ·𝑠 ‘ 𝑀 ) 𝐼 ) = ( ( 𝑞 ( ·𝑠 ‘ 𝑀 ) 𝐼 ) ( +g ‘ 𝑀 ) ( 𝑟 ( ·𝑠 ‘ 𝑀 ) 𝐼 ) ) ) ∧ ( ( ( 𝑞 ( .r ‘ ( Scalar ‘ 𝑀 ) ) 𝑟 ) ( ·𝑠 ‘ 𝑀 ) 𝐼 ) = ( 𝑞 ( ·𝑠 ‘ 𝑀 ) ( 𝑟 ( ·𝑠 ‘ 𝑀 ) 𝐼 ) ) ∧ ( ( 1r ‘ ( Scalar ‘ 𝑀 ) ) ( ·𝑠 ‘ 𝑀 ) 𝐼 ) = 𝐼 ) ) ) )
89	88	2ralbidv	⊢ ( ( 𝐼 ∈ 𝑉 ∧ 𝑅 ∈ Ring ) → ( ∀ 𝑞 ∈ ( Base ‘ ( Scalar ‘ 𝑀 ) ) ∀ 𝑟 ∈ ( Base ‘ ( Scalar ‘ 𝑀 ) ) ∀ 𝑥 ∈ { 𝐼 } ∀ 𝑤 ∈ { 𝐼 } ( ( ( 𝑟 ( ·𝑠 ‘ 𝑀 ) 𝑤 ) ∈ { 𝐼 } ∧ ( 𝑟 ( ·𝑠 ‘ 𝑀 ) ( 𝑤 ( +g ‘ 𝑀 ) 𝑥 ) ) = ( ( 𝑟 ( ·𝑠 ‘ 𝑀 ) 𝑤 ) ( +g ‘ 𝑀 ) ( 𝑟 ( ·𝑠 ‘ 𝑀 ) 𝑥 ) ) ∧ ( ( 𝑞 ( +g ‘ ( Scalar ‘ 𝑀 ) ) 𝑟 ) ( ·𝑠 ‘ 𝑀 ) 𝑤 ) = ( ( 𝑞 ( ·𝑠 ‘ 𝑀 ) 𝑤 ) ( +g ‘ 𝑀 ) ( 𝑟 ( ·𝑠 ‘ 𝑀 ) 𝑤 ) ) ) ∧ ( ( ( 𝑞 ( .r ‘ ( Scalar ‘ 𝑀 ) ) 𝑟 ) ( ·𝑠 ‘ 𝑀 ) 𝑤 ) = ( 𝑞 ( ·𝑠 ‘ 𝑀 ) ( 𝑟 ( ·𝑠 ‘ 𝑀 ) 𝑤 ) ) ∧ ( ( 1r ‘ ( Scalar ‘ 𝑀 ) ) ( ·𝑠 ‘ 𝑀 ) 𝑤 ) = 𝑤 ) ) ↔ ∀ 𝑞 ∈ ( Base ‘ ( Scalar ‘ 𝑀 ) ) ∀ 𝑟 ∈ ( Base ‘ ( Scalar ‘ 𝑀 ) ) ( ( ( 𝑟 ( ·𝑠 ‘ 𝑀 ) 𝐼 ) ∈ { 𝐼 } ∧ ( 𝑟 ( ·𝑠 ‘ 𝑀 ) ( 𝐼 ( +g ‘ 𝑀 ) 𝐼 ) ) = ( ( 𝑟 ( ·𝑠 ‘ 𝑀 ) 𝐼 ) ( +g ‘ 𝑀 ) ( 𝑟 ( ·𝑠 ‘ 𝑀 ) 𝐼 ) ) ∧ ( ( 𝑞 ( +g ‘ ( Scalar ‘ 𝑀 ) ) 𝑟 ) ( ·𝑠 ‘ 𝑀 ) 𝐼 ) = ( ( 𝑞 ( ·𝑠 ‘ 𝑀 ) 𝐼 ) ( +g ‘ 𝑀 ) ( 𝑟 ( ·𝑠 ‘ 𝑀 ) 𝐼 ) ) ) ∧ ( ( ( 𝑞 ( .r ‘ ( Scalar ‘ 𝑀 ) ) 𝑟 ) ( ·𝑠 ‘ 𝑀 ) 𝐼 ) = ( 𝑞 ( ·𝑠 ‘ 𝑀 ) ( 𝑟 ( ·𝑠 ‘ 𝑀 ) 𝐼 ) ) ∧ ( ( 1r ‘ ( Scalar ‘ 𝑀 ) ) ( ·𝑠 ‘ 𝑀 ) 𝐼 ) = 𝐼 ) ) ) )
90	56 89	mpbird	⊢ ( ( 𝐼 ∈ 𝑉 ∧ 𝑅 ∈ Ring ) → ∀ 𝑞 ∈ ( Base ‘ ( Scalar ‘ 𝑀 ) ) ∀ 𝑟 ∈ ( Base ‘ ( Scalar ‘ 𝑀 ) ) ∀ 𝑥 ∈ { 𝐼 } ∀ 𝑤 ∈ { 𝐼 } ( ( ( 𝑟 ( ·𝑠 ‘ 𝑀 ) 𝑤 ) ∈ { 𝐼 } ∧ ( 𝑟 ( ·𝑠 ‘ 𝑀 ) ( 𝑤 ( +g ‘ 𝑀 ) 𝑥 ) ) = ( ( 𝑟 ( ·𝑠 ‘ 𝑀 ) 𝑤 ) ( +g ‘ 𝑀 ) ( 𝑟 ( ·𝑠 ‘ 𝑀 ) 𝑥 ) ) ∧ ( ( 𝑞 ( +g ‘ ( Scalar ‘ 𝑀 ) ) 𝑟 ) ( ·𝑠 ‘ 𝑀 ) 𝑤 ) = ( ( 𝑞 ( ·𝑠 ‘ 𝑀 ) 𝑤 ) ( +g ‘ 𝑀 ) ( 𝑟 ( ·𝑠 ‘ 𝑀 ) 𝑤 ) ) ) ∧ ( ( ( 𝑞 ( .r ‘ ( Scalar ‘ 𝑀 ) ) 𝑟 ) ( ·𝑠 ‘ 𝑀 ) 𝑤 ) = ( 𝑞 ( ·𝑠 ‘ 𝑀 ) ( 𝑟 ( ·𝑠 ‘ 𝑀 ) 𝑤 ) ) ∧ ( ( 1r ‘ ( Scalar ‘ 𝑀 ) ) ( ·𝑠 ‘ 𝑀 ) 𝑤 ) = 𝑤 ) ) )
91	1	lmodbase	⊢ ( { 𝐼 } ∈ V → { 𝐼 } = ( Base ‘ 𝑀 ) )
92	5 91	ax-mp	⊢ { 𝐼 } = ( Base ‘ 𝑀 )
93		eqid	⊢ ( +g ‘ 𝑀 ) = ( +g ‘ 𝑀 )
94		eqid	⊢ ( ·𝑠 ‘ 𝑀 ) = ( ·𝑠 ‘ 𝑀 )
95		eqid	⊢ ( Scalar ‘ 𝑀 ) = ( Scalar ‘ 𝑀 )
96		eqid	⊢ ( Base ‘ ( Scalar ‘ 𝑀 ) ) = ( Base ‘ ( Scalar ‘ 𝑀 ) )
97		eqid	⊢ ( +g ‘ ( Scalar ‘ 𝑀 ) ) = ( +g ‘ ( Scalar ‘ 𝑀 ) )
98		eqid	⊢ ( .r ‘ ( Scalar ‘ 𝑀 ) ) = ( .r ‘ ( Scalar ‘ 𝑀 ) )
99		eqid	⊢ ( 1r ‘ ( Scalar ‘ 𝑀 ) ) = ( 1r ‘ ( Scalar ‘ 𝑀 ) )
100	92 93 94 95 96 97 98 99	islmod	⊢ ( 𝑀 ∈ LMod ↔ ( 𝑀 ∈ Grp ∧ ( Scalar ‘ 𝑀 ) ∈ Ring ∧ ∀ 𝑞 ∈ ( Base ‘ ( Scalar ‘ 𝑀 ) ) ∀ 𝑟 ∈ ( Base ‘ ( Scalar ‘ 𝑀 ) ) ∀ 𝑥 ∈ { 𝐼 } ∀ 𝑤 ∈ { 𝐼 } ( ( ( 𝑟 ( ·𝑠 ‘ 𝑀 ) 𝑤 ) ∈ { 𝐼 } ∧ ( 𝑟 ( ·𝑠 ‘ 𝑀 ) ( 𝑤 ( +g ‘ 𝑀 ) 𝑥 ) ) = ( ( 𝑟 ( ·𝑠 ‘ 𝑀 ) 𝑤 ) ( +g ‘ 𝑀 ) ( 𝑟 ( ·𝑠 ‘ 𝑀 ) 𝑥 ) ) ∧ ( ( 𝑞 ( +g ‘ ( Scalar ‘ 𝑀 ) ) 𝑟 ) ( ·𝑠 ‘ 𝑀 ) 𝑤 ) = ( ( 𝑞 ( ·𝑠 ‘ 𝑀 ) 𝑤 ) ( +g ‘ 𝑀 ) ( 𝑟 ( ·𝑠 ‘ 𝑀 ) 𝑤 ) ) ) ∧ ( ( ( 𝑞 ( .r ‘ ( Scalar ‘ 𝑀 ) ) 𝑟 ) ( ·𝑠 ‘ 𝑀 ) 𝑤 ) = ( 𝑞 ( ·𝑠 ‘ 𝑀 ) ( 𝑟 ( ·𝑠 ‘ 𝑀 ) 𝑤 ) ) ∧ ( ( 1r ‘ ( Scalar ‘ 𝑀 ) ) ( ·𝑠 ‘ 𝑀 ) 𝑤 ) = 𝑤 ) ) ) )
101	30 35 90 100	syl3anbrc	⊢ ( ( 𝐼 ∈ 𝑉 ∧ 𝑅 ∈ Ring ) → 𝑀 ∈ LMod )