Metamath Proof Explorer

Theorem erngdvlem3-rN

Description: Lemma for eringring . (Contributed by NM, 6-Aug-2013) (New usage is discouraged.)

Ref Expression
Hypotheses ernggrp.h-r ⊢ 𝐻 = ( LHyp ‘ 𝐾 )
ernggrp.d-r ⊢ 𝐷 = ( ( EDRingR ‘ 𝐾 ) ‘ 𝑊 )
ernggrplem.b-r ⊢ 𝐵 = ( Base ‘ 𝐾 )
ernggrplem.t-r ⊢ 𝑇 = ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 )
ernggrplem.e-r ⊢ 𝐸 = ( ( TEndo ‘ 𝐾 ) ‘ 𝑊 )
ernggrplem.p-r ⊢ 𝑃 = ( 𝑎 ∈ 𝐸 , 𝑏 ∈ 𝐸 ↦ ( 𝑓 ∈ 𝑇 ↦ ( ( 𝑎 ‘ 𝑓 ) ∘ ( 𝑏 ‘ 𝑓 ) ) ) )
ernggrplem.o-r ⊢ 𝑂 = ( 𝑓 ∈ 𝑇 ↦ ( I ↾ 𝐵 ) )
ernggrplem.i-r ⊢ 𝐼 = ( 𝑎 ∈ 𝐸 ↦ ( 𝑓 ∈ 𝑇 ↦ ◡ ( 𝑎 ‘ 𝑓 ) ) )
erngrnglem.m-r ⊢ 𝑀 = ( 𝑎 ∈ 𝐸 , 𝑏 ∈ 𝐸 ↦ ( 𝑏 ∘ 𝑎 ) )
Assertion erngdvlem3-rN ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) → 𝐷 ∈ Ring )

Proof

Step Hyp Ref Expression
1 ernggrp.h-r ⊢ 𝐻 = ( LHyp ‘ 𝐾 )
2 ernggrp.d-r ⊢ 𝐷 = ( ( EDRingR ‘ 𝐾 ) ‘ 𝑊 )
3 ernggrplem.b-r ⊢ 𝐵 = ( Base ‘ 𝐾 )
4 ernggrplem.t-r ⊢ 𝑇 = ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 )
5 ernggrplem.e-r ⊢ 𝐸 = ( ( TEndo ‘ 𝐾 ) ‘ 𝑊 )
6 ernggrplem.p-r ⊢ 𝑃 = ( 𝑎 ∈ 𝐸 , 𝑏 ∈ 𝐸 ↦ ( 𝑓 ∈ 𝑇 ↦ ( ( 𝑎 ‘ 𝑓 ) ∘ ( 𝑏 ‘ 𝑓 ) ) ) )
7 ernggrplem.o-r ⊢ 𝑂 = ( 𝑓 ∈ 𝑇 ↦ ( I ↾ 𝐵 ) )
8 ernggrplem.i-r ⊢ 𝐼 = ( 𝑎 ∈ 𝐸 ↦ ( 𝑓 ∈ 𝑇 ↦ ◡ ( 𝑎 ‘ 𝑓 ) ) )
9 erngrnglem.m-r ⊢ 𝑀 = ( 𝑎 ∈ 𝐸 , 𝑏 ∈ 𝐸 ↦ ( 𝑏 ∘ 𝑎 ) )
10 eqid ⊢ ( Base ‘ 𝐷 ) = ( Base ‘ 𝐷 )
11 1 4 5 2 10 erngbase-rN ⊢ ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) → ( Base ‘ 𝐷 ) = 𝐸 )
12 11 eqcomd ⊢ ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) → 𝐸 = ( Base ‘ 𝐷 ) )
13 eqid ⊢ ( +g ‘ 𝐷 ) = ( +g ‘ 𝐷 )
14 1 4 5 2 13 erngfplus-rN ⊢ ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) → ( +g ‘ 𝐷 ) = ( 𝑎 ∈ 𝐸 , 𝑏 ∈ 𝐸 ↦ ( 𝑓 ∈ 𝑇 ↦ ( ( 𝑎 ‘ 𝑓 ) ∘ ( 𝑏 ‘ 𝑓 ) ) ) ) )
15 6 14 eqtr4id ⊢ ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) → 𝑃 = ( +g ‘ 𝐷 ) )
16 eqid ⊢ ( .r ‘ 𝐷 ) = ( .r ‘ 𝐷 )
17 1 4 5 2 16 erngfmul-rN ⊢ ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) → ( .r ‘ 𝐷 ) = ( 𝑎 ∈ 𝐸 , 𝑏 ∈ 𝐸 ↦ ( 𝑏 ∘ 𝑎 ) ) )
18 9 17 eqtr4id ⊢ ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) → 𝑀 = ( .r ‘ 𝐷 ) )
19 1 2 3 4 5 6 7 8 erngdvlem1-rN ⊢ ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) → 𝐷 ∈ Grp )
20 18 oveqd ⊢ ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) → ( 𝑠 𝑀 𝑡 ) = ( 𝑠 ( .r ‘ 𝐷 ) 𝑡 ) )
21 20 3ad2ant1 ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑠 ∈ 𝐸 ∧ 𝑡 ∈ 𝐸 ) → ( 𝑠 𝑀 𝑡 ) = ( 𝑠 ( .r ‘ 𝐷 ) 𝑡 ) )
22 1 4 5 2 16 erngmul-rN ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑠 ∈ 𝐸 ∧ 𝑡 ∈ 𝐸 ) ) → ( 𝑠 ( .r ‘ 𝐷 ) 𝑡 ) = ( 𝑡 ∘ 𝑠 ) )
23 22 3impb ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑠 ∈ 𝐸 ∧ 𝑡 ∈ 𝐸 ) → ( 𝑠 ( .r ‘ 𝐷 ) 𝑡 ) = ( 𝑡 ∘ 𝑠 ) )
24 21 23 eqtrd ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑠 ∈ 𝐸 ∧ 𝑡 ∈ 𝐸 ) → ( 𝑠 𝑀 𝑡 ) = ( 𝑡 ∘ 𝑠 ) )
25 1 5 tendococl ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑡 ∈ 𝐸 ∧ 𝑠 ∈ 𝐸 ) → ( 𝑡 ∘ 𝑠 ) ∈ 𝐸 )
26 25 3com23 ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑠 ∈ 𝐸 ∧ 𝑡 ∈ 𝐸 ) → ( 𝑡 ∘ 𝑠 ) ∈ 𝐸 )
27 24 26 eqeltrd ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑠 ∈ 𝐸 ∧ 𝑡 ∈ 𝐸 ) → ( 𝑠 𝑀 𝑡 ) ∈ 𝐸 )
28 18 oveqdr ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑠 ∈ 𝐸 ∧ 𝑡 ∈ 𝐸 ∧ 𝑢 ∈ 𝐸 ) ) → ( 𝑡 𝑀 𝑢 ) = ( 𝑡 ( .r ‘ 𝐷 ) 𝑢 ) )
29 1 4 5 2 16 erngmul-rN ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑡 ∈ 𝐸 ∧ 𝑢 ∈ 𝐸 ) ) → ( 𝑡 ( .r ‘ 𝐷 ) 𝑢 ) = ( 𝑢 ∘ 𝑡 ) )
30 29 3adantr1 ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑠 ∈ 𝐸 ∧ 𝑡 ∈ 𝐸 ∧ 𝑢 ∈ 𝐸 ) ) → ( 𝑡 ( .r ‘ 𝐷 ) 𝑢 ) = ( 𝑢 ∘ 𝑡 ) )
31 28 30 eqtrd ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑠 ∈ 𝐸 ∧ 𝑡 ∈ 𝐸 ∧ 𝑢 ∈ 𝐸 ) ) → ( 𝑡 𝑀 𝑢 ) = ( 𝑢 ∘ 𝑡 ) )
32 31 coeq1d ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑠 ∈ 𝐸 ∧ 𝑡 ∈ 𝐸 ∧ 𝑢 ∈ 𝐸 ) ) → ( ( 𝑡 𝑀 𝑢 ) ∘ 𝑠 ) = ( ( 𝑢 ∘ 𝑡 ) ∘ 𝑠 ) )
33 18 oveqd ⊢ ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) → ( 𝑠 𝑀 ( 𝑡 𝑀 𝑢 ) ) = ( 𝑠 ( .r ‘ 𝐷 ) ( 𝑡 𝑀 𝑢 ) ) )
34 33 adantr ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑠 ∈ 𝐸 ∧ 𝑡 ∈ 𝐸 ∧ 𝑢 ∈ 𝐸 ) ) → ( 𝑠 𝑀 ( 𝑡 𝑀 𝑢 ) ) = ( 𝑠 ( .r ‘ 𝐷 ) ( 𝑡 𝑀 𝑢 ) ) )
35 simpl ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑠 ∈ 𝐸 ∧ 𝑡 ∈ 𝐸 ∧ 𝑢 ∈ 𝐸 ) ) → ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) )
36 simpr1 ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑠 ∈ 𝐸 ∧ 𝑡 ∈ 𝐸 ∧ 𝑢 ∈ 𝐸 ) ) → 𝑠 ∈ 𝐸 )
37 simpr3 ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑠 ∈ 𝐸 ∧ 𝑡 ∈ 𝐸 ∧ 𝑢 ∈ 𝐸 ) ) → 𝑢 ∈ 𝐸 )
38 simpr2 ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑠 ∈ 𝐸 ∧ 𝑡 ∈ 𝐸 ∧ 𝑢 ∈ 𝐸 ) ) → 𝑡 ∈ 𝐸 )
39 1 5 tendococl ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑢 ∈ 𝐸 ∧ 𝑡 ∈ 𝐸 ) → ( 𝑢 ∘ 𝑡 ) ∈ 𝐸 )
40 35 37 38 39 syl3anc ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑠 ∈ 𝐸 ∧ 𝑡 ∈ 𝐸 ∧ 𝑢 ∈ 𝐸 ) ) → ( 𝑢 ∘ 𝑡 ) ∈ 𝐸 )
41 31 40 eqeltrd ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑠 ∈ 𝐸 ∧ 𝑡 ∈ 𝐸 ∧ 𝑢 ∈ 𝐸 ) ) → ( 𝑡 𝑀 𝑢 ) ∈ 𝐸 )
42 1 4 5 2 16 erngmul-rN ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑠 ∈ 𝐸 ∧ ( 𝑡 𝑀 𝑢 ) ∈ 𝐸 ) ) → ( 𝑠 ( .r ‘ 𝐷 ) ( 𝑡 𝑀 𝑢 ) ) = ( ( 𝑡 𝑀 𝑢 ) ∘ 𝑠 ) )
43 35 36 41 42 syl12anc ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑠 ∈ 𝐸 ∧ 𝑡 ∈ 𝐸 ∧ 𝑢 ∈ 𝐸 ) ) → ( 𝑠 ( .r ‘ 𝐷 ) ( 𝑡 𝑀 𝑢 ) ) = ( ( 𝑡 𝑀 𝑢 ) ∘ 𝑠 ) )
44 34 43 eqtrd ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑠 ∈ 𝐸 ∧ 𝑡 ∈ 𝐸 ∧ 𝑢 ∈ 𝐸 ) ) → ( 𝑠 𝑀 ( 𝑡 𝑀 𝑢 ) ) = ( ( 𝑡 𝑀 𝑢 ) ∘ 𝑠 ) )
45 18 oveqd ⊢ ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) → ( ( 𝑠 𝑀 𝑡 ) 𝑀 𝑢 ) = ( ( 𝑠 𝑀 𝑡 ) ( .r ‘ 𝐷 ) 𝑢 ) )
46 45 adantr ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑠 ∈ 𝐸 ∧ 𝑡 ∈ 𝐸 ∧ 𝑢 ∈ 𝐸 ) ) → ( ( 𝑠 𝑀 𝑡 ) 𝑀 𝑢 ) = ( ( 𝑠 𝑀 𝑡 ) ( .r ‘ 𝐷 ) 𝑢 ) )
47 27 3adant3r3 ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑠 ∈ 𝐸 ∧ 𝑡 ∈ 𝐸 ∧ 𝑢 ∈ 𝐸 ) ) → ( 𝑠 𝑀 𝑡 ) ∈ 𝐸 )
48 1 4 5 2 16 erngmul-rN ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( ( 𝑠 𝑀 𝑡 ) ∈ 𝐸 ∧ 𝑢 ∈ 𝐸 ) ) → ( ( 𝑠 𝑀 𝑡 ) ( .r ‘ 𝐷 ) 𝑢 ) = ( 𝑢 ∘ ( 𝑠 𝑀 𝑡 ) ) )
49 35 47 37 48 syl12anc ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑠 ∈ 𝐸 ∧ 𝑡 ∈ 𝐸 ∧ 𝑢 ∈ 𝐸 ) ) → ( ( 𝑠 𝑀 𝑡 ) ( .r ‘ 𝐷 ) 𝑢 ) = ( 𝑢 ∘ ( 𝑠 𝑀 𝑡 ) ) )
50 18 oveqdr ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑠 ∈ 𝐸 ∧ 𝑡 ∈ 𝐸 ∧ 𝑢 ∈ 𝐸 ) ) → ( 𝑠 𝑀 𝑡 ) = ( 𝑠 ( .r ‘ 𝐷 ) 𝑡 ) )
51 22 3adantr3 ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑠 ∈ 𝐸 ∧ 𝑡 ∈ 𝐸 ∧ 𝑢 ∈ 𝐸 ) ) → ( 𝑠 ( .r ‘ 𝐷 ) 𝑡 ) = ( 𝑡 ∘ 𝑠 ) )
52 50 51 eqtrd ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑠 ∈ 𝐸 ∧ 𝑡 ∈ 𝐸 ∧ 𝑢 ∈ 𝐸 ) ) → ( 𝑠 𝑀 𝑡 ) = ( 𝑡 ∘ 𝑠 ) )
53 52 coeq2d ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑠 ∈ 𝐸 ∧ 𝑡 ∈ 𝐸 ∧ 𝑢 ∈ 𝐸 ) ) → ( 𝑢 ∘ ( 𝑠 𝑀 𝑡 ) ) = ( 𝑢 ∘ ( 𝑡 ∘ 𝑠 ) ) )
54 46 49 53 3eqtrd ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑠 ∈ 𝐸 ∧ 𝑡 ∈ 𝐸 ∧ 𝑢 ∈ 𝐸 ) ) → ( ( 𝑠 𝑀 𝑡 ) 𝑀 𝑢 ) = ( 𝑢 ∘ ( 𝑡 ∘ 𝑠 ) ) )
55 coass ⊢ ( ( 𝑢 ∘ 𝑡 ) ∘ 𝑠 ) = ( 𝑢 ∘ ( 𝑡 ∘ 𝑠 ) )
56 54 55 eqtr4di ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑠 ∈ 𝐸 ∧ 𝑡 ∈ 𝐸 ∧ 𝑢 ∈ 𝐸 ) ) → ( ( 𝑠 𝑀 𝑡 ) 𝑀 𝑢 ) = ( ( 𝑢 ∘ 𝑡 ) ∘ 𝑠 ) )
57 32 44 56 3eqtr4rd ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑠 ∈ 𝐸 ∧ 𝑡 ∈ 𝐸 ∧ 𝑢 ∈ 𝐸 ) ) → ( ( 𝑠 𝑀 𝑡 ) 𝑀 𝑢 ) = ( 𝑠 𝑀 ( 𝑡 𝑀 𝑢 ) ) )
58 1 4 5 6 tendodi2 ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑡 ∈ 𝐸 ∧ 𝑢 ∈ 𝐸 ∧ 𝑠 ∈ 𝐸 ) ) → ( ( 𝑡 𝑃 𝑢 ) ∘ 𝑠 ) = ( ( 𝑡 ∘ 𝑠 ) 𝑃 ( 𝑢 ∘ 𝑠 ) ) )
59 35 38 37 36 58 syl13anc ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑠 ∈ 𝐸 ∧ 𝑡 ∈ 𝐸 ∧ 𝑢 ∈ 𝐸 ) ) → ( ( 𝑡 𝑃 𝑢 ) ∘ 𝑠 ) = ( ( 𝑡 ∘ 𝑠 ) 𝑃 ( 𝑢 ∘ 𝑠 ) ) )
60 18 oveqd ⊢ ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) → ( 𝑠 𝑀 ( 𝑡 𝑃 𝑢 ) ) = ( 𝑠 ( .r ‘ 𝐷 ) ( 𝑡 𝑃 𝑢 ) ) )
61 60 adantr ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑠 ∈ 𝐸 ∧ 𝑡 ∈ 𝐸 ∧ 𝑢 ∈ 𝐸 ) ) → ( 𝑠 𝑀 ( 𝑡 𝑃 𝑢 ) ) = ( 𝑠 ( .r ‘ 𝐷 ) ( 𝑡 𝑃 𝑢 ) ) )
62 1 4 5 6 tendoplcl ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑡 ∈ 𝐸 ∧ 𝑢 ∈ 𝐸 ) → ( 𝑡 𝑃 𝑢 ) ∈ 𝐸 )
63 35 38 37 62 syl3anc ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑠 ∈ 𝐸 ∧ 𝑡 ∈ 𝐸 ∧ 𝑢 ∈ 𝐸 ) ) → ( 𝑡 𝑃 𝑢 ) ∈ 𝐸 )
64 1 4 5 2 16 erngmul-rN ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑠 ∈ 𝐸 ∧ ( 𝑡 𝑃 𝑢 ) ∈ 𝐸 ) ) → ( 𝑠 ( .r ‘ 𝐷 ) ( 𝑡 𝑃 𝑢 ) ) = ( ( 𝑡 𝑃 𝑢 ) ∘ 𝑠 ) )
65 35 36 63 64 syl12anc ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑠 ∈ 𝐸 ∧ 𝑡 ∈ 𝐸 ∧ 𝑢 ∈ 𝐸 ) ) → ( 𝑠 ( .r ‘ 𝐷 ) ( 𝑡 𝑃 𝑢 ) ) = ( ( 𝑡 𝑃 𝑢 ) ∘ 𝑠 ) )
66 61 65 eqtrd ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑠 ∈ 𝐸 ∧ 𝑡 ∈ 𝐸 ∧ 𝑢 ∈ 𝐸 ) ) → ( 𝑠 𝑀 ( 𝑡 𝑃 𝑢 ) ) = ( ( 𝑡 𝑃 𝑢 ) ∘ 𝑠 ) )
67 18 oveqdr ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑠 ∈ 𝐸 ∧ 𝑡 ∈ 𝐸 ∧ 𝑢 ∈ 𝐸 ) ) → ( 𝑠 𝑀 𝑢 ) = ( 𝑠 ( .r ‘ 𝐷 ) 𝑢 ) )
68 1 4 5 2 16 erngmul-rN ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑠 ∈ 𝐸 ∧ 𝑢 ∈ 𝐸 ) ) → ( 𝑠 ( .r ‘ 𝐷 ) 𝑢 ) = ( 𝑢 ∘ 𝑠 ) )
69 68 3adantr2 ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑠 ∈ 𝐸 ∧ 𝑡 ∈ 𝐸 ∧ 𝑢 ∈ 𝐸 ) ) → ( 𝑠 ( .r ‘ 𝐷 ) 𝑢 ) = ( 𝑢 ∘ 𝑠 ) )
70 67 69 eqtrd ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑠 ∈ 𝐸 ∧ 𝑡 ∈ 𝐸 ∧ 𝑢 ∈ 𝐸 ) ) → ( 𝑠 𝑀 𝑢 ) = ( 𝑢 ∘ 𝑠 ) )
71 52 70 oveq12d ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑠 ∈ 𝐸 ∧ 𝑡 ∈ 𝐸 ∧ 𝑢 ∈ 𝐸 ) ) → ( ( 𝑠 𝑀 𝑡 ) 𝑃 ( 𝑠 𝑀 𝑢 ) ) = ( ( 𝑡 ∘ 𝑠 ) 𝑃 ( 𝑢 ∘ 𝑠 ) ) )
72 59 66 71 3eqtr4d ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑠 ∈ 𝐸 ∧ 𝑡 ∈ 𝐸 ∧ 𝑢 ∈ 𝐸 ) ) → ( 𝑠 𝑀 ( 𝑡 𝑃 𝑢 ) ) = ( ( 𝑠 𝑀 𝑡 ) 𝑃 ( 𝑠 𝑀 𝑢 ) ) )
73 1 4 5 6 tendodi1 ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑢 ∈ 𝐸 ∧ 𝑠 ∈ 𝐸 ∧ 𝑡 ∈ 𝐸 ) ) → ( 𝑢 ∘ ( 𝑠 𝑃 𝑡 ) ) = ( ( 𝑢 ∘ 𝑠 ) 𝑃 ( 𝑢 ∘ 𝑡 ) ) )
74 35 37 36 38 73 syl13anc ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑠 ∈ 𝐸 ∧ 𝑡 ∈ 𝐸 ∧ 𝑢 ∈ 𝐸 ) ) → ( 𝑢 ∘ ( 𝑠 𝑃 𝑡 ) ) = ( ( 𝑢 ∘ 𝑠 ) 𝑃 ( 𝑢 ∘ 𝑡 ) ) )
75 18 adantr ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑠 ∈ 𝐸 ∧ 𝑡 ∈ 𝐸 ∧ 𝑢 ∈ 𝐸 ) ) → 𝑀 = ( .r ‘ 𝐷 ) )
76 75 oveqd ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑠 ∈ 𝐸 ∧ 𝑡 ∈ 𝐸 ∧ 𝑢 ∈ 𝐸 ) ) → ( ( 𝑠 𝑃 𝑡 ) 𝑀 𝑢 ) = ( ( 𝑠 𝑃 𝑡 ) ( .r ‘ 𝐷 ) 𝑢 ) )
77 1 4 5 6 tendoplcl ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑠 ∈ 𝐸 ∧ 𝑡 ∈ 𝐸 ) → ( 𝑠 𝑃 𝑡 ) ∈ 𝐸 )
78 77 3adant3r3 ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑠 ∈ 𝐸 ∧ 𝑡 ∈ 𝐸 ∧ 𝑢 ∈ 𝐸 ) ) → ( 𝑠 𝑃 𝑡 ) ∈ 𝐸 )
79 1 4 5 2 16 erngmul-rN ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( ( 𝑠 𝑃 𝑡 ) ∈ 𝐸 ∧ 𝑢 ∈ 𝐸 ) ) → ( ( 𝑠 𝑃 𝑡 ) ( .r ‘ 𝐷 ) 𝑢 ) = ( 𝑢 ∘ ( 𝑠 𝑃 𝑡 ) ) )
80 35 78 37 79 syl12anc ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑠 ∈ 𝐸 ∧ 𝑡 ∈ 𝐸 ∧ 𝑢 ∈ 𝐸 ) ) → ( ( 𝑠 𝑃 𝑡 ) ( .r ‘ 𝐷 ) 𝑢 ) = ( 𝑢 ∘ ( 𝑠 𝑃 𝑡 ) ) )
81 76 80 eqtrd ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑠 ∈ 𝐸 ∧ 𝑡 ∈ 𝐸 ∧ 𝑢 ∈ 𝐸 ) ) → ( ( 𝑠 𝑃 𝑡 ) 𝑀 𝑢 ) = ( 𝑢 ∘ ( 𝑠 𝑃 𝑡 ) ) )
82 70 31 oveq12d ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑠 ∈ 𝐸 ∧ 𝑡 ∈ 𝐸 ∧ 𝑢 ∈ 𝐸 ) ) → ( ( 𝑠 𝑀 𝑢 ) 𝑃 ( 𝑡 𝑀 𝑢 ) ) = ( ( 𝑢 ∘ 𝑠 ) 𝑃 ( 𝑢 ∘ 𝑡 ) ) )
83 74 81 82 3eqtr4d ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑠 ∈ 𝐸 ∧ 𝑡 ∈ 𝐸 ∧ 𝑢 ∈ 𝐸 ) ) → ( ( 𝑠 𝑃 𝑡 ) 𝑀 𝑢 ) = ( ( 𝑠 𝑀 𝑢 ) 𝑃 ( 𝑡 𝑀 𝑢 ) ) )
84 1 4 5 tendoidcl ⊢ ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) → ( I ↾ 𝑇 ) ∈ 𝐸 )
85 18 oveqd ⊢ ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) → ( ( I ↾ 𝑇 ) 𝑀 𝑠 ) = ( ( I ↾ 𝑇 ) ( .r ‘ 𝐷 ) 𝑠 ) )
86 85 adantr ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑠 ∈ 𝐸 ) → ( ( I ↾ 𝑇 ) 𝑀 𝑠 ) = ( ( I ↾ 𝑇 ) ( .r ‘ 𝐷 ) 𝑠 ) )
87 simpl ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑠 ∈ 𝐸 ) → ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) )
88 84 adantr ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑠 ∈ 𝐸 ) → ( I ↾ 𝑇 ) ∈ 𝐸 )
89 simpr ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑠 ∈ 𝐸 ) → 𝑠 ∈ 𝐸 )
90 1 4 5 2 16 erngmul-rN ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( ( I ↾ 𝑇 ) ∈ 𝐸 ∧ 𝑠 ∈ 𝐸 ) ) → ( ( I ↾ 𝑇 ) ( .r ‘ 𝐷 ) 𝑠 ) = ( 𝑠 ∘ ( I ↾ 𝑇 ) ) )
91 87 88 89 90 syl12anc ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑠 ∈ 𝐸 ) → ( ( I ↾ 𝑇 ) ( .r ‘ 𝐷 ) 𝑠 ) = ( 𝑠 ∘ ( I ↾ 𝑇 ) ) )
92 1 4 5 tendo1mulr ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑠 ∈ 𝐸 ) → ( 𝑠 ∘ ( I ↾ 𝑇 ) ) = 𝑠 )
93 86 91 92 3eqtrd ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑠 ∈ 𝐸 ) → ( ( I ↾ 𝑇 ) 𝑀 𝑠 ) = 𝑠 )
94 18 oveqd ⊢ ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) → ( 𝑠 𝑀 ( I ↾ 𝑇 ) ) = ( 𝑠 ( .r ‘ 𝐷 ) ( I ↾ 𝑇 ) ) )
95 94 adantr ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑠 ∈ 𝐸 ) → ( 𝑠 𝑀 ( I ↾ 𝑇 ) ) = ( 𝑠 ( .r ‘ 𝐷 ) ( I ↾ 𝑇 ) ) )
96 1 4 5 2 16 erngmul-rN ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑠 ∈ 𝐸 ∧ ( I ↾ 𝑇 ) ∈ 𝐸 ) ) → ( 𝑠 ( .r ‘ 𝐷 ) ( I ↾ 𝑇 ) ) = ( ( I ↾ 𝑇 ) ∘ 𝑠 ) )
97 87 89 88 96 syl12anc ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑠 ∈ 𝐸 ) → ( 𝑠 ( .r ‘ 𝐷 ) ( I ↾ 𝑇 ) ) = ( ( I ↾ 𝑇 ) ∘ 𝑠 ) )
98 1 4 5 tendo1mul ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑠 ∈ 𝐸 ) → ( ( I ↾ 𝑇 ) ∘ 𝑠 ) = 𝑠 )
99 95 97 98 3eqtrd ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑠 ∈ 𝐸 ) → ( 𝑠 𝑀 ( I ↾ 𝑇 ) ) = 𝑠 )
100 12 15 18 19 27 57 72 83 84 93 99 isringd ⊢ ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) → 𝐷 ∈ Ring )