Theorem assamulgscmlem1

Description: Lemma 1 for assamulgscm (induction base). (Contributed by AV, 26-Aug-2019)

	Ref	Expression
Hypotheses	assamulgscm.v	⊢ 𝑉 = ( Base ‘ 𝑊 )
	assamulgscm.f	⊢ 𝐹 = ( Scalar ‘ 𝑊 )
	assamulgscm.b	⊢ 𝐵 = ( Base ‘ 𝐹 )
	assamulgscm.s	⊢ · = ( ·𝑠 ‘ 𝑊 )
	assamulgscm.g	⊢ 𝐺 = ( mulGrp ‘ 𝐹 )
	assamulgscm.p	⊢ ↑ = ( .g ‘ 𝐺 )
	assamulgscm.h	⊢ 𝐻 = ( mulGrp ‘ 𝑊 )
	assamulgscm.e	⊢ 𝐸 = ( .g ‘ 𝐻 )
Assertion	assamulgscmlem1	⊢ ( ( ( 𝐴 ∈ 𝐵 ∧ 𝑋 ∈ 𝑉 ) ∧ 𝑊 ∈ AssAlg ) → ( 0 𝐸 ( 𝐴 · 𝑋 ) ) = ( ( 0 ↑ 𝐴 ) · ( 0 𝐸 𝑋 ) ) )

Proof

Step	Hyp	Ref	Expression
1		assamulgscm.v	⊢ 𝑉 = ( Base ‘ 𝑊 )
2		assamulgscm.f	⊢ 𝐹 = ( Scalar ‘ 𝑊 )
3		assamulgscm.b	⊢ 𝐵 = ( Base ‘ 𝐹 )
4		assamulgscm.s	⊢ · = ( ·𝑠 ‘ 𝑊 )
5		assamulgscm.g	⊢ 𝐺 = ( mulGrp ‘ 𝐹 )
6		assamulgscm.p	⊢ ↑ = ( .g ‘ 𝐺 )
7		assamulgscm.h	⊢ 𝐻 = ( mulGrp ‘ 𝑊 )
8		assamulgscm.e	⊢ 𝐸 = ( .g ‘ 𝐻 )
9		assalmod	⊢ ( 𝑊 ∈ AssAlg → 𝑊 ∈ LMod )
10		assaring	⊢ ( 𝑊 ∈ AssAlg → 𝑊 ∈ Ring )
11		eqid	⊢ ( 1r ‘ 𝑊 ) = ( 1r ‘ 𝑊 )
12	1 11	ringidcl	⊢ ( 𝑊 ∈ Ring → ( 1r ‘ 𝑊 ) ∈ 𝑉 )
13	10 12	syl	⊢ ( 𝑊 ∈ AssAlg → ( 1r ‘ 𝑊 ) ∈ 𝑉 )
14		eqid	⊢ ( 1r ‘ 𝐹 ) = ( 1r ‘ 𝐹 )
15	1 2 4 14	lmodvs1	⊢ ( ( 𝑊 ∈ LMod ∧ ( 1r ‘ 𝑊 ) ∈ 𝑉 ) → ( ( 1r ‘ 𝐹 ) · ( 1r ‘ 𝑊 ) ) = ( 1r ‘ 𝑊 ) )
16	15	eqcomd	⊢ ( ( 𝑊 ∈ LMod ∧ ( 1r ‘ 𝑊 ) ∈ 𝑉 ) → ( 1r ‘ 𝑊 ) = ( ( 1r ‘ 𝐹 ) · ( 1r ‘ 𝑊 ) ) )
17	9 13 16	syl2anc	⊢ ( 𝑊 ∈ AssAlg → ( 1r ‘ 𝑊 ) = ( ( 1r ‘ 𝐹 ) · ( 1r ‘ 𝑊 ) ) )
18	17	adantl	⊢ ( ( ( 𝐴 ∈ 𝐵 ∧ 𝑋 ∈ 𝑉 ) ∧ 𝑊 ∈ AssAlg ) → ( 1r ‘ 𝑊 ) = ( ( 1r ‘ 𝐹 ) · ( 1r ‘ 𝑊 ) ) )
19	9	adantl	⊢ ( ( ( 𝐴 ∈ 𝐵 ∧ 𝑋 ∈ 𝑉 ) ∧ 𝑊 ∈ AssAlg ) → 𝑊 ∈ LMod )
20		simpll	⊢ ( ( ( 𝐴 ∈ 𝐵 ∧ 𝑋 ∈ 𝑉 ) ∧ 𝑊 ∈ AssAlg ) → 𝐴 ∈ 𝐵 )
21		simplr	⊢ ( ( ( 𝐴 ∈ 𝐵 ∧ 𝑋 ∈ 𝑉 ) ∧ 𝑊 ∈ AssAlg ) → 𝑋 ∈ 𝑉 )
22	1 2 4 3	lmodvscl	⊢ ( ( 𝑊 ∈ LMod ∧ 𝐴 ∈ 𝐵 ∧ 𝑋 ∈ 𝑉 ) → ( 𝐴 · 𝑋 ) ∈ 𝑉 )
23	19 20 21 22	syl3anc	⊢ ( ( ( 𝐴 ∈ 𝐵 ∧ 𝑋 ∈ 𝑉 ) ∧ 𝑊 ∈ AssAlg ) → ( 𝐴 · 𝑋 ) ∈ 𝑉 )
24	7 1	mgpbas	⊢ 𝑉 = ( Base ‘ 𝐻 )
25	7 11	ringidval	⊢ ( 1r ‘ 𝑊 ) = ( 0g ‘ 𝐻 )
26	24 25 8	mulg0	⊢ ( ( 𝐴 · 𝑋 ) ∈ 𝑉 → ( 0 𝐸 ( 𝐴 · 𝑋 ) ) = ( 1r ‘ 𝑊 ) )
27	23 26	syl	⊢ ( ( ( 𝐴 ∈ 𝐵 ∧ 𝑋 ∈ 𝑉 ) ∧ 𝑊 ∈ AssAlg ) → ( 0 𝐸 ( 𝐴 · 𝑋 ) ) = ( 1r ‘ 𝑊 ) )
28	5 3	mgpbas	⊢ 𝐵 = ( Base ‘ 𝐺 )
29	5 14	ringidval	⊢ ( 1r ‘ 𝐹 ) = ( 0g ‘ 𝐺 )
30	28 29 6	mulg0	⊢ ( 𝐴 ∈ 𝐵 → ( 0 ↑ 𝐴 ) = ( 1r ‘ 𝐹 ) )
31	20 30	syl	⊢ ( ( ( 𝐴 ∈ 𝐵 ∧ 𝑋 ∈ 𝑉 ) ∧ 𝑊 ∈ AssAlg ) → ( 0 ↑ 𝐴 ) = ( 1r ‘ 𝐹 ) )
32	24 25 8	mulg0	⊢ ( 𝑋 ∈ 𝑉 → ( 0 𝐸 𝑋 ) = ( 1r ‘ 𝑊 ) )
33	21 32	syl	⊢ ( ( ( 𝐴 ∈ 𝐵 ∧ 𝑋 ∈ 𝑉 ) ∧ 𝑊 ∈ AssAlg ) → ( 0 𝐸 𝑋 ) = ( 1r ‘ 𝑊 ) )
34	31 33	oveq12d	⊢ ( ( ( 𝐴 ∈ 𝐵 ∧ 𝑋 ∈ 𝑉 ) ∧ 𝑊 ∈ AssAlg ) → ( ( 0 ↑ 𝐴 ) · ( 0 𝐸 𝑋 ) ) = ( ( 1r ‘ 𝐹 ) · ( 1r ‘ 𝑊 ) ) )
35	18 27 34	3eqtr4d	⊢ ( ( ( 𝐴 ∈ 𝐵 ∧ 𝑋 ∈ 𝑉 ) ∧ 𝑊 ∈ AssAlg ) → ( 0 𝐸 ( 𝐴 · 𝑋 ) ) = ( ( 0 ↑ 𝐴 ) · ( 0 𝐸 𝑋 ) ) )