This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 𝐸 𝑋 ) ) )