Step |
Hyp |
Ref |
Expression |
1 |
|
dvhgrp.b |
⊢ 𝐵 = ( Base ‘ 𝐾 ) |
2 |
|
dvhgrp.h |
⊢ 𝐻 = ( LHyp ‘ 𝐾 ) |
3 |
|
dvhgrp.t |
⊢ 𝑇 = ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) |
4 |
|
dvhgrp.e |
⊢ 𝐸 = ( ( TEndo ‘ 𝐾 ) ‘ 𝑊 ) |
5 |
|
dvhgrp.u |
⊢ 𝑈 = ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 ) |
6 |
|
dvhgrp.d |
⊢ 𝐷 = ( Scalar ‘ 𝑈 ) |
7 |
|
dvhgrp.p |
⊢ ⨣ = ( +g ‘ 𝐷 ) |
8 |
|
dvhgrp.a |
⊢ + = ( +g ‘ 𝑈 ) |
9 |
|
dvhgrp.o |
⊢ 0 = ( 0g ‘ 𝐷 ) |
10 |
|
dvhgrp.i |
⊢ 𝐼 = ( invg ‘ 𝐷 ) |
11 |
|
dvhlvec.m |
⊢ × = ( .r ‘ 𝐷 ) |
12 |
|
dvhlvec.s |
⊢ · = ( ·𝑠 ‘ 𝑈 ) |
13 |
|
eqid |
⊢ ( Base ‘ 𝑈 ) = ( Base ‘ 𝑈 ) |
14 |
2 3 4 5 13
|
dvhvbase |
⊢ ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) → ( Base ‘ 𝑈 ) = ( 𝑇 × 𝐸 ) ) |
15 |
14
|
eqcomd |
⊢ ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) → ( 𝑇 × 𝐸 ) = ( Base ‘ 𝑈 ) ) |
16 |
8
|
a1i |
⊢ ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) → + = ( +g ‘ 𝑈 ) ) |
17 |
6
|
a1i |
⊢ ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) → 𝐷 = ( Scalar ‘ 𝑈 ) ) |
18 |
12
|
a1i |
⊢ ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) → · = ( ·𝑠 ‘ 𝑈 ) ) |
19 |
|
eqid |
⊢ ( Base ‘ 𝐷 ) = ( Base ‘ 𝐷 ) |
20 |
2 4 5 6 19
|
dvhbase |
⊢ ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) → ( Base ‘ 𝐷 ) = 𝐸 ) |
21 |
20
|
eqcomd |
⊢ ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) → 𝐸 = ( Base ‘ 𝐷 ) ) |
22 |
7
|
a1i |
⊢ ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) → ⨣ = ( +g ‘ 𝐷 ) ) |
23 |
11
|
a1i |
⊢ ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) → × = ( .r ‘ 𝐷 ) ) |
24 |
|
eqid |
⊢ ( ( EDRing ‘ 𝐾 ) ‘ 𝑊 ) = ( ( EDRing ‘ 𝐾 ) ‘ 𝑊 ) |
25 |
2 24 5 6
|
dvhsca |
⊢ ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) → 𝐷 = ( ( EDRing ‘ 𝐾 ) ‘ 𝑊 ) ) |
26 |
25
|
fveq2d |
⊢ ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) → ( 1r ‘ 𝐷 ) = ( 1r ‘ ( ( EDRing ‘ 𝐾 ) ‘ 𝑊 ) ) ) |
27 |
|
eqid |
⊢ ( 1r ‘ ( ( EDRing ‘ 𝐾 ) ‘ 𝑊 ) ) = ( 1r ‘ ( ( EDRing ‘ 𝐾 ) ‘ 𝑊 ) ) |
28 |
2 3 24 27
|
erng1r |
⊢ ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) → ( 1r ‘ ( ( EDRing ‘ 𝐾 ) ‘ 𝑊 ) ) = ( I ↾ 𝑇 ) ) |
29 |
26 28
|
eqtr2d |
⊢ ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) → ( I ↾ 𝑇 ) = ( 1r ‘ 𝐷 ) ) |
30 |
2 24
|
erngdv |
⊢ ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) → ( ( EDRing ‘ 𝐾 ) ‘ 𝑊 ) ∈ DivRing ) |
31 |
25 30
|
eqeltrd |
⊢ ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) → 𝐷 ∈ DivRing ) |
32 |
|
drngring |
⊢ ( 𝐷 ∈ DivRing → 𝐷 ∈ Ring ) |
33 |
31 32
|
syl |
⊢ ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) → 𝐷 ∈ Ring ) |
34 |
1 2 3 4 5 6 7 8 9 10
|
dvhgrp |
⊢ ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) → 𝑈 ∈ Grp ) |
35 |
2 3 4 5 12
|
dvhvscacl |
⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑠 ∈ 𝐸 ∧ 𝑡 ∈ ( 𝑇 × 𝐸 ) ) ) → ( 𝑠 · 𝑡 ) ∈ ( 𝑇 × 𝐸 ) ) |
36 |
35
|
3impb |
⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑠 ∈ 𝐸 ∧ 𝑡 ∈ ( 𝑇 × 𝐸 ) ) → ( 𝑠 · 𝑡 ) ∈ ( 𝑇 × 𝐸 ) ) |
37 |
|
simpl |
⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑠 ∈ 𝐸 ∧ 𝑡 ∈ ( 𝑇 × 𝐸 ) ∧ 𝑓 ∈ ( 𝑇 × 𝐸 ) ) ) → ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ) |
38 |
|
simpr1 |
⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑠 ∈ 𝐸 ∧ 𝑡 ∈ ( 𝑇 × 𝐸 ) ∧ 𝑓 ∈ ( 𝑇 × 𝐸 ) ) ) → 𝑠 ∈ 𝐸 ) |
39 |
|
simpr2 |
⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑠 ∈ 𝐸 ∧ 𝑡 ∈ ( 𝑇 × 𝐸 ) ∧ 𝑓 ∈ ( 𝑇 × 𝐸 ) ) ) → 𝑡 ∈ ( 𝑇 × 𝐸 ) ) |
40 |
|
xp1st |
⊢ ( 𝑡 ∈ ( 𝑇 × 𝐸 ) → ( 1st ‘ 𝑡 ) ∈ 𝑇 ) |
41 |
39 40
|
syl |
⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑠 ∈ 𝐸 ∧ 𝑡 ∈ ( 𝑇 × 𝐸 ) ∧ 𝑓 ∈ ( 𝑇 × 𝐸 ) ) ) → ( 1st ‘ 𝑡 ) ∈ 𝑇 ) |
42 |
|
simpr3 |
⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑠 ∈ 𝐸 ∧ 𝑡 ∈ ( 𝑇 × 𝐸 ) ∧ 𝑓 ∈ ( 𝑇 × 𝐸 ) ) ) → 𝑓 ∈ ( 𝑇 × 𝐸 ) ) |
43 |
|
xp1st |
⊢ ( 𝑓 ∈ ( 𝑇 × 𝐸 ) → ( 1st ‘ 𝑓 ) ∈ 𝑇 ) |
44 |
42 43
|
syl |
⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑠 ∈ 𝐸 ∧ 𝑡 ∈ ( 𝑇 × 𝐸 ) ∧ 𝑓 ∈ ( 𝑇 × 𝐸 ) ) ) → ( 1st ‘ 𝑓 ) ∈ 𝑇 ) |
45 |
2 3 4
|
tendospdi1 |
⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑠 ∈ 𝐸 ∧ ( 1st ‘ 𝑡 ) ∈ 𝑇 ∧ ( 1st ‘ 𝑓 ) ∈ 𝑇 ) ) → ( 𝑠 ‘ ( ( 1st ‘ 𝑡 ) ∘ ( 1st ‘ 𝑓 ) ) ) = ( ( 𝑠 ‘ ( 1st ‘ 𝑡 ) ) ∘ ( 𝑠 ‘ ( 1st ‘ 𝑓 ) ) ) ) |
46 |
37 38 41 44 45
|
syl13anc |
⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑠 ∈ 𝐸 ∧ 𝑡 ∈ ( 𝑇 × 𝐸 ) ∧ 𝑓 ∈ ( 𝑇 × 𝐸 ) ) ) → ( 𝑠 ‘ ( ( 1st ‘ 𝑡 ) ∘ ( 1st ‘ 𝑓 ) ) ) = ( ( 𝑠 ‘ ( 1st ‘ 𝑡 ) ) ∘ ( 𝑠 ‘ ( 1st ‘ 𝑓 ) ) ) ) |
47 |
2 3 4 5 6 8 7
|
dvhvadd |
⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑡 ∈ ( 𝑇 × 𝐸 ) ∧ 𝑓 ∈ ( 𝑇 × 𝐸 ) ) ) → ( 𝑡 + 𝑓 ) = 〈 ( ( 1st ‘ 𝑡 ) ∘ ( 1st ‘ 𝑓 ) ) , ( ( 2nd ‘ 𝑡 ) ⨣ ( 2nd ‘ 𝑓 ) ) 〉 ) |
48 |
47
|
3adantr1 |
⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑠 ∈ 𝐸 ∧ 𝑡 ∈ ( 𝑇 × 𝐸 ) ∧ 𝑓 ∈ ( 𝑇 × 𝐸 ) ) ) → ( 𝑡 + 𝑓 ) = 〈 ( ( 1st ‘ 𝑡 ) ∘ ( 1st ‘ 𝑓 ) ) , ( ( 2nd ‘ 𝑡 ) ⨣ ( 2nd ‘ 𝑓 ) ) 〉 ) |
49 |
48
|
fveq2d |
⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑠 ∈ 𝐸 ∧ 𝑡 ∈ ( 𝑇 × 𝐸 ) ∧ 𝑓 ∈ ( 𝑇 × 𝐸 ) ) ) → ( 1st ‘ ( 𝑡 + 𝑓 ) ) = ( 1st ‘ 〈 ( ( 1st ‘ 𝑡 ) ∘ ( 1st ‘ 𝑓 ) ) , ( ( 2nd ‘ 𝑡 ) ⨣ ( 2nd ‘ 𝑓 ) ) 〉 ) ) |
50 |
|
fvex |
⊢ ( 1st ‘ 𝑡 ) ∈ V |
51 |
|
fvex |
⊢ ( 1st ‘ 𝑓 ) ∈ V |
52 |
50 51
|
coex |
⊢ ( ( 1st ‘ 𝑡 ) ∘ ( 1st ‘ 𝑓 ) ) ∈ V |
53 |
|
ovex |
⊢ ( ( 2nd ‘ 𝑡 ) ⨣ ( 2nd ‘ 𝑓 ) ) ∈ V |
54 |
52 53
|
op1st |
⊢ ( 1st ‘ 〈 ( ( 1st ‘ 𝑡 ) ∘ ( 1st ‘ 𝑓 ) ) , ( ( 2nd ‘ 𝑡 ) ⨣ ( 2nd ‘ 𝑓 ) ) 〉 ) = ( ( 1st ‘ 𝑡 ) ∘ ( 1st ‘ 𝑓 ) ) |
55 |
49 54
|
eqtrdi |
⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑠 ∈ 𝐸 ∧ 𝑡 ∈ ( 𝑇 × 𝐸 ) ∧ 𝑓 ∈ ( 𝑇 × 𝐸 ) ) ) → ( 1st ‘ ( 𝑡 + 𝑓 ) ) = ( ( 1st ‘ 𝑡 ) ∘ ( 1st ‘ 𝑓 ) ) ) |
56 |
55
|
fveq2d |
⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑠 ∈ 𝐸 ∧ 𝑡 ∈ ( 𝑇 × 𝐸 ) ∧ 𝑓 ∈ ( 𝑇 × 𝐸 ) ) ) → ( 𝑠 ‘ ( 1st ‘ ( 𝑡 + 𝑓 ) ) ) = ( 𝑠 ‘ ( ( 1st ‘ 𝑡 ) ∘ ( 1st ‘ 𝑓 ) ) ) ) |
57 |
2 3 4 5 12
|
dvhvsca |
⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑠 ∈ 𝐸 ∧ 𝑡 ∈ ( 𝑇 × 𝐸 ) ) ) → ( 𝑠 · 𝑡 ) = 〈 ( 𝑠 ‘ ( 1st ‘ 𝑡 ) ) , ( 𝑠 ∘ ( 2nd ‘ 𝑡 ) ) 〉 ) |
58 |
57
|
3adantr3 |
⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑠 ∈ 𝐸 ∧ 𝑡 ∈ ( 𝑇 × 𝐸 ) ∧ 𝑓 ∈ ( 𝑇 × 𝐸 ) ) ) → ( 𝑠 · 𝑡 ) = 〈 ( 𝑠 ‘ ( 1st ‘ 𝑡 ) ) , ( 𝑠 ∘ ( 2nd ‘ 𝑡 ) ) 〉 ) |
59 |
58
|
fveq2d |
⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑠 ∈ 𝐸 ∧ 𝑡 ∈ ( 𝑇 × 𝐸 ) ∧ 𝑓 ∈ ( 𝑇 × 𝐸 ) ) ) → ( 1st ‘ ( 𝑠 · 𝑡 ) ) = ( 1st ‘ 〈 ( 𝑠 ‘ ( 1st ‘ 𝑡 ) ) , ( 𝑠 ∘ ( 2nd ‘ 𝑡 ) ) 〉 ) ) |
60 |
|
fvex |
⊢ ( 𝑠 ‘ ( 1st ‘ 𝑡 ) ) ∈ V |
61 |
|
vex |
⊢ 𝑠 ∈ V |
62 |
|
fvex |
⊢ ( 2nd ‘ 𝑡 ) ∈ V |
63 |
61 62
|
coex |
⊢ ( 𝑠 ∘ ( 2nd ‘ 𝑡 ) ) ∈ V |
64 |
60 63
|
op1st |
⊢ ( 1st ‘ 〈 ( 𝑠 ‘ ( 1st ‘ 𝑡 ) ) , ( 𝑠 ∘ ( 2nd ‘ 𝑡 ) ) 〉 ) = ( 𝑠 ‘ ( 1st ‘ 𝑡 ) ) |
65 |
59 64
|
eqtrdi |
⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑠 ∈ 𝐸 ∧ 𝑡 ∈ ( 𝑇 × 𝐸 ) ∧ 𝑓 ∈ ( 𝑇 × 𝐸 ) ) ) → ( 1st ‘ ( 𝑠 · 𝑡 ) ) = ( 𝑠 ‘ ( 1st ‘ 𝑡 ) ) ) |
66 |
2 3 4 5 12
|
dvhvsca |
⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑠 ∈ 𝐸 ∧ 𝑓 ∈ ( 𝑇 × 𝐸 ) ) ) → ( 𝑠 · 𝑓 ) = 〈 ( 𝑠 ‘ ( 1st ‘ 𝑓 ) ) , ( 𝑠 ∘ ( 2nd ‘ 𝑓 ) ) 〉 ) |
67 |
66
|
3adantr2 |
⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑠 ∈ 𝐸 ∧ 𝑡 ∈ ( 𝑇 × 𝐸 ) ∧ 𝑓 ∈ ( 𝑇 × 𝐸 ) ) ) → ( 𝑠 · 𝑓 ) = 〈 ( 𝑠 ‘ ( 1st ‘ 𝑓 ) ) , ( 𝑠 ∘ ( 2nd ‘ 𝑓 ) ) 〉 ) |
68 |
67
|
fveq2d |
⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑠 ∈ 𝐸 ∧ 𝑡 ∈ ( 𝑇 × 𝐸 ) ∧ 𝑓 ∈ ( 𝑇 × 𝐸 ) ) ) → ( 1st ‘ ( 𝑠 · 𝑓 ) ) = ( 1st ‘ 〈 ( 𝑠 ‘ ( 1st ‘ 𝑓 ) ) , ( 𝑠 ∘ ( 2nd ‘ 𝑓 ) ) 〉 ) ) |
69 |
|
fvex |
⊢ ( 𝑠 ‘ ( 1st ‘ 𝑓 ) ) ∈ V |
70 |
|
fvex |
⊢ ( 2nd ‘ 𝑓 ) ∈ V |
71 |
61 70
|
coex |
⊢ ( 𝑠 ∘ ( 2nd ‘ 𝑓 ) ) ∈ V |
72 |
69 71
|
op1st |
⊢ ( 1st ‘ 〈 ( 𝑠 ‘ ( 1st ‘ 𝑓 ) ) , ( 𝑠 ∘ ( 2nd ‘ 𝑓 ) ) 〉 ) = ( 𝑠 ‘ ( 1st ‘ 𝑓 ) ) |
73 |
68 72
|
eqtrdi |
⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑠 ∈ 𝐸 ∧ 𝑡 ∈ ( 𝑇 × 𝐸 ) ∧ 𝑓 ∈ ( 𝑇 × 𝐸 ) ) ) → ( 1st ‘ ( 𝑠 · 𝑓 ) ) = ( 𝑠 ‘ ( 1st ‘ 𝑓 ) ) ) |
74 |
65 73
|
coeq12d |
⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑠 ∈ 𝐸 ∧ 𝑡 ∈ ( 𝑇 × 𝐸 ) ∧ 𝑓 ∈ ( 𝑇 × 𝐸 ) ) ) → ( ( 1st ‘ ( 𝑠 · 𝑡 ) ) ∘ ( 1st ‘ ( 𝑠 · 𝑓 ) ) ) = ( ( 𝑠 ‘ ( 1st ‘ 𝑡 ) ) ∘ ( 𝑠 ‘ ( 1st ‘ 𝑓 ) ) ) ) |
75 |
46 56 74
|
3eqtr4d |
⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑠 ∈ 𝐸 ∧ 𝑡 ∈ ( 𝑇 × 𝐸 ) ∧ 𝑓 ∈ ( 𝑇 × 𝐸 ) ) ) → ( 𝑠 ‘ ( 1st ‘ ( 𝑡 + 𝑓 ) ) ) = ( ( 1st ‘ ( 𝑠 · 𝑡 ) ) ∘ ( 1st ‘ ( 𝑠 · 𝑓 ) ) ) ) |
76 |
33
|
adantr |
⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑠 ∈ 𝐸 ∧ 𝑡 ∈ ( 𝑇 × 𝐸 ) ∧ 𝑓 ∈ ( 𝑇 × 𝐸 ) ) ) → 𝐷 ∈ Ring ) |
77 |
21
|
adantr |
⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑠 ∈ 𝐸 ∧ 𝑡 ∈ ( 𝑇 × 𝐸 ) ∧ 𝑓 ∈ ( 𝑇 × 𝐸 ) ) ) → 𝐸 = ( Base ‘ 𝐷 ) ) |
78 |
38 77
|
eleqtrd |
⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑠 ∈ 𝐸 ∧ 𝑡 ∈ ( 𝑇 × 𝐸 ) ∧ 𝑓 ∈ ( 𝑇 × 𝐸 ) ) ) → 𝑠 ∈ ( Base ‘ 𝐷 ) ) |
79 |
|
xp2nd |
⊢ ( 𝑡 ∈ ( 𝑇 × 𝐸 ) → ( 2nd ‘ 𝑡 ) ∈ 𝐸 ) |
80 |
39 79
|
syl |
⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑠 ∈ 𝐸 ∧ 𝑡 ∈ ( 𝑇 × 𝐸 ) ∧ 𝑓 ∈ ( 𝑇 × 𝐸 ) ) ) → ( 2nd ‘ 𝑡 ) ∈ 𝐸 ) |
81 |
80 77
|
eleqtrd |
⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑠 ∈ 𝐸 ∧ 𝑡 ∈ ( 𝑇 × 𝐸 ) ∧ 𝑓 ∈ ( 𝑇 × 𝐸 ) ) ) → ( 2nd ‘ 𝑡 ) ∈ ( Base ‘ 𝐷 ) ) |
82 |
|
xp2nd |
⊢ ( 𝑓 ∈ ( 𝑇 × 𝐸 ) → ( 2nd ‘ 𝑓 ) ∈ 𝐸 ) |
83 |
42 82
|
syl |
⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑠 ∈ 𝐸 ∧ 𝑡 ∈ ( 𝑇 × 𝐸 ) ∧ 𝑓 ∈ ( 𝑇 × 𝐸 ) ) ) → ( 2nd ‘ 𝑓 ) ∈ 𝐸 ) |
84 |
83 77
|
eleqtrd |
⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑠 ∈ 𝐸 ∧ 𝑡 ∈ ( 𝑇 × 𝐸 ) ∧ 𝑓 ∈ ( 𝑇 × 𝐸 ) ) ) → ( 2nd ‘ 𝑓 ) ∈ ( Base ‘ 𝐷 ) ) |
85 |
19 7 11
|
ringdi |
⊢ ( ( 𝐷 ∈ Ring ∧ ( 𝑠 ∈ ( Base ‘ 𝐷 ) ∧ ( 2nd ‘ 𝑡 ) ∈ ( Base ‘ 𝐷 ) ∧ ( 2nd ‘ 𝑓 ) ∈ ( Base ‘ 𝐷 ) ) ) → ( 𝑠 × ( ( 2nd ‘ 𝑡 ) ⨣ ( 2nd ‘ 𝑓 ) ) ) = ( ( 𝑠 × ( 2nd ‘ 𝑡 ) ) ⨣ ( 𝑠 × ( 2nd ‘ 𝑓 ) ) ) ) |
86 |
76 78 81 84 85
|
syl13anc |
⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑠 ∈ 𝐸 ∧ 𝑡 ∈ ( 𝑇 × 𝐸 ) ∧ 𝑓 ∈ ( 𝑇 × 𝐸 ) ) ) → ( 𝑠 × ( ( 2nd ‘ 𝑡 ) ⨣ ( 2nd ‘ 𝑓 ) ) ) = ( ( 𝑠 × ( 2nd ‘ 𝑡 ) ) ⨣ ( 𝑠 × ( 2nd ‘ 𝑓 ) ) ) ) |
87 |
19 7
|
ringacl |
⊢ ( ( 𝐷 ∈ Ring ∧ ( 2nd ‘ 𝑡 ) ∈ ( Base ‘ 𝐷 ) ∧ ( 2nd ‘ 𝑓 ) ∈ ( Base ‘ 𝐷 ) ) → ( ( 2nd ‘ 𝑡 ) ⨣ ( 2nd ‘ 𝑓 ) ) ∈ ( Base ‘ 𝐷 ) ) |
88 |
76 81 84 87
|
syl3anc |
⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑠 ∈ 𝐸 ∧ 𝑡 ∈ ( 𝑇 × 𝐸 ) ∧ 𝑓 ∈ ( 𝑇 × 𝐸 ) ) ) → ( ( 2nd ‘ 𝑡 ) ⨣ ( 2nd ‘ 𝑓 ) ) ∈ ( Base ‘ 𝐷 ) ) |
89 |
88 77
|
eleqtrrd |
⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑠 ∈ 𝐸 ∧ 𝑡 ∈ ( 𝑇 × 𝐸 ) ∧ 𝑓 ∈ ( 𝑇 × 𝐸 ) ) ) → ( ( 2nd ‘ 𝑡 ) ⨣ ( 2nd ‘ 𝑓 ) ) ∈ 𝐸 ) |
90 |
2 3 4 5 6 11
|
dvhmulr |
⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑠 ∈ 𝐸 ∧ ( ( 2nd ‘ 𝑡 ) ⨣ ( 2nd ‘ 𝑓 ) ) ∈ 𝐸 ) ) → ( 𝑠 × ( ( 2nd ‘ 𝑡 ) ⨣ ( 2nd ‘ 𝑓 ) ) ) = ( 𝑠 ∘ ( ( 2nd ‘ 𝑡 ) ⨣ ( 2nd ‘ 𝑓 ) ) ) ) |
91 |
37 38 89 90
|
syl12anc |
⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑠 ∈ 𝐸 ∧ 𝑡 ∈ ( 𝑇 × 𝐸 ) ∧ 𝑓 ∈ ( 𝑇 × 𝐸 ) ) ) → ( 𝑠 × ( ( 2nd ‘ 𝑡 ) ⨣ ( 2nd ‘ 𝑓 ) ) ) = ( 𝑠 ∘ ( ( 2nd ‘ 𝑡 ) ⨣ ( 2nd ‘ 𝑓 ) ) ) ) |
92 |
2 3 4 5 6 11
|
dvhmulr |
⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑠 ∈ 𝐸 ∧ ( 2nd ‘ 𝑡 ) ∈ 𝐸 ) ) → ( 𝑠 × ( 2nd ‘ 𝑡 ) ) = ( 𝑠 ∘ ( 2nd ‘ 𝑡 ) ) ) |
93 |
37 38 80 92
|
syl12anc |
⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑠 ∈ 𝐸 ∧ 𝑡 ∈ ( 𝑇 × 𝐸 ) ∧ 𝑓 ∈ ( 𝑇 × 𝐸 ) ) ) → ( 𝑠 × ( 2nd ‘ 𝑡 ) ) = ( 𝑠 ∘ ( 2nd ‘ 𝑡 ) ) ) |
94 |
2 3 4 5 6 11
|
dvhmulr |
⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑠 ∈ 𝐸 ∧ ( 2nd ‘ 𝑓 ) ∈ 𝐸 ) ) → ( 𝑠 × ( 2nd ‘ 𝑓 ) ) = ( 𝑠 ∘ ( 2nd ‘ 𝑓 ) ) ) |
95 |
37 38 83 94
|
syl12anc |
⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑠 ∈ 𝐸 ∧ 𝑡 ∈ ( 𝑇 × 𝐸 ) ∧ 𝑓 ∈ ( 𝑇 × 𝐸 ) ) ) → ( 𝑠 × ( 2nd ‘ 𝑓 ) ) = ( 𝑠 ∘ ( 2nd ‘ 𝑓 ) ) ) |
96 |
93 95
|
oveq12d |
⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑠 ∈ 𝐸 ∧ 𝑡 ∈ ( 𝑇 × 𝐸 ) ∧ 𝑓 ∈ ( 𝑇 × 𝐸 ) ) ) → ( ( 𝑠 × ( 2nd ‘ 𝑡 ) ) ⨣ ( 𝑠 × ( 2nd ‘ 𝑓 ) ) ) = ( ( 𝑠 ∘ ( 2nd ‘ 𝑡 ) ) ⨣ ( 𝑠 ∘ ( 2nd ‘ 𝑓 ) ) ) ) |
97 |
86 91 96
|
3eqtr3d |
⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑠 ∈ 𝐸 ∧ 𝑡 ∈ ( 𝑇 × 𝐸 ) ∧ 𝑓 ∈ ( 𝑇 × 𝐸 ) ) ) → ( 𝑠 ∘ ( ( 2nd ‘ 𝑡 ) ⨣ ( 2nd ‘ 𝑓 ) ) ) = ( ( 𝑠 ∘ ( 2nd ‘ 𝑡 ) ) ⨣ ( 𝑠 ∘ ( 2nd ‘ 𝑓 ) ) ) ) |
98 |
48
|
fveq2d |
⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑠 ∈ 𝐸 ∧ 𝑡 ∈ ( 𝑇 × 𝐸 ) ∧ 𝑓 ∈ ( 𝑇 × 𝐸 ) ) ) → ( 2nd ‘ ( 𝑡 + 𝑓 ) ) = ( 2nd ‘ 〈 ( ( 1st ‘ 𝑡 ) ∘ ( 1st ‘ 𝑓 ) ) , ( ( 2nd ‘ 𝑡 ) ⨣ ( 2nd ‘ 𝑓 ) ) 〉 ) ) |
99 |
52 53
|
op2nd |
⊢ ( 2nd ‘ 〈 ( ( 1st ‘ 𝑡 ) ∘ ( 1st ‘ 𝑓 ) ) , ( ( 2nd ‘ 𝑡 ) ⨣ ( 2nd ‘ 𝑓 ) ) 〉 ) = ( ( 2nd ‘ 𝑡 ) ⨣ ( 2nd ‘ 𝑓 ) ) |
100 |
98 99
|
eqtrdi |
⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑠 ∈ 𝐸 ∧ 𝑡 ∈ ( 𝑇 × 𝐸 ) ∧ 𝑓 ∈ ( 𝑇 × 𝐸 ) ) ) → ( 2nd ‘ ( 𝑡 + 𝑓 ) ) = ( ( 2nd ‘ 𝑡 ) ⨣ ( 2nd ‘ 𝑓 ) ) ) |
101 |
100
|
coeq2d |
⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑠 ∈ 𝐸 ∧ 𝑡 ∈ ( 𝑇 × 𝐸 ) ∧ 𝑓 ∈ ( 𝑇 × 𝐸 ) ) ) → ( 𝑠 ∘ ( 2nd ‘ ( 𝑡 + 𝑓 ) ) ) = ( 𝑠 ∘ ( ( 2nd ‘ 𝑡 ) ⨣ ( 2nd ‘ 𝑓 ) ) ) ) |
102 |
58
|
fveq2d |
⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑠 ∈ 𝐸 ∧ 𝑡 ∈ ( 𝑇 × 𝐸 ) ∧ 𝑓 ∈ ( 𝑇 × 𝐸 ) ) ) → ( 2nd ‘ ( 𝑠 · 𝑡 ) ) = ( 2nd ‘ 〈 ( 𝑠 ‘ ( 1st ‘ 𝑡 ) ) , ( 𝑠 ∘ ( 2nd ‘ 𝑡 ) ) 〉 ) ) |
103 |
60 63
|
op2nd |
⊢ ( 2nd ‘ 〈 ( 𝑠 ‘ ( 1st ‘ 𝑡 ) ) , ( 𝑠 ∘ ( 2nd ‘ 𝑡 ) ) 〉 ) = ( 𝑠 ∘ ( 2nd ‘ 𝑡 ) ) |
104 |
102 103
|
eqtrdi |
⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑠 ∈ 𝐸 ∧ 𝑡 ∈ ( 𝑇 × 𝐸 ) ∧ 𝑓 ∈ ( 𝑇 × 𝐸 ) ) ) → ( 2nd ‘ ( 𝑠 · 𝑡 ) ) = ( 𝑠 ∘ ( 2nd ‘ 𝑡 ) ) ) |
105 |
67
|
fveq2d |
⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑠 ∈ 𝐸 ∧ 𝑡 ∈ ( 𝑇 × 𝐸 ) ∧ 𝑓 ∈ ( 𝑇 × 𝐸 ) ) ) → ( 2nd ‘ ( 𝑠 · 𝑓 ) ) = ( 2nd ‘ 〈 ( 𝑠 ‘ ( 1st ‘ 𝑓 ) ) , ( 𝑠 ∘ ( 2nd ‘ 𝑓 ) ) 〉 ) ) |
106 |
69 71
|
op2nd |
⊢ ( 2nd ‘ 〈 ( 𝑠 ‘ ( 1st ‘ 𝑓 ) ) , ( 𝑠 ∘ ( 2nd ‘ 𝑓 ) ) 〉 ) = ( 𝑠 ∘ ( 2nd ‘ 𝑓 ) ) |
107 |
105 106
|
eqtrdi |
⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑠 ∈ 𝐸 ∧ 𝑡 ∈ ( 𝑇 × 𝐸 ) ∧ 𝑓 ∈ ( 𝑇 × 𝐸 ) ) ) → ( 2nd ‘ ( 𝑠 · 𝑓 ) ) = ( 𝑠 ∘ ( 2nd ‘ 𝑓 ) ) ) |
108 |
104 107
|
oveq12d |
⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑠 ∈ 𝐸 ∧ 𝑡 ∈ ( 𝑇 × 𝐸 ) ∧ 𝑓 ∈ ( 𝑇 × 𝐸 ) ) ) → ( ( 2nd ‘ ( 𝑠 · 𝑡 ) ) ⨣ ( 2nd ‘ ( 𝑠 · 𝑓 ) ) ) = ( ( 𝑠 ∘ ( 2nd ‘ 𝑡 ) ) ⨣ ( 𝑠 ∘ ( 2nd ‘ 𝑓 ) ) ) ) |
109 |
97 101 108
|
3eqtr4d |
⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑠 ∈ 𝐸 ∧ 𝑡 ∈ ( 𝑇 × 𝐸 ) ∧ 𝑓 ∈ ( 𝑇 × 𝐸 ) ) ) → ( 𝑠 ∘ ( 2nd ‘ ( 𝑡 + 𝑓 ) ) ) = ( ( 2nd ‘ ( 𝑠 · 𝑡 ) ) ⨣ ( 2nd ‘ ( 𝑠 · 𝑓 ) ) ) ) |
110 |
75 109
|
opeq12d |
⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑠 ∈ 𝐸 ∧ 𝑡 ∈ ( 𝑇 × 𝐸 ) ∧ 𝑓 ∈ ( 𝑇 × 𝐸 ) ) ) → 〈 ( 𝑠 ‘ ( 1st ‘ ( 𝑡 + 𝑓 ) ) ) , ( 𝑠 ∘ ( 2nd ‘ ( 𝑡 + 𝑓 ) ) ) 〉 = 〈 ( ( 1st ‘ ( 𝑠 · 𝑡 ) ) ∘ ( 1st ‘ ( 𝑠 · 𝑓 ) ) ) , ( ( 2nd ‘ ( 𝑠 · 𝑡 ) ) ⨣ ( 2nd ‘ ( 𝑠 · 𝑓 ) ) ) 〉 ) |
111 |
2 3 4 5 6 7 8
|
dvhvaddcl |
⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑡 ∈ ( 𝑇 × 𝐸 ) ∧ 𝑓 ∈ ( 𝑇 × 𝐸 ) ) ) → ( 𝑡 + 𝑓 ) ∈ ( 𝑇 × 𝐸 ) ) |
112 |
111
|
3adantr1 |
⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑠 ∈ 𝐸 ∧ 𝑡 ∈ ( 𝑇 × 𝐸 ) ∧ 𝑓 ∈ ( 𝑇 × 𝐸 ) ) ) → ( 𝑡 + 𝑓 ) ∈ ( 𝑇 × 𝐸 ) ) |
113 |
2 3 4 5 12
|
dvhvsca |
⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑠 ∈ 𝐸 ∧ ( 𝑡 + 𝑓 ) ∈ ( 𝑇 × 𝐸 ) ) ) → ( 𝑠 · ( 𝑡 + 𝑓 ) ) = 〈 ( 𝑠 ‘ ( 1st ‘ ( 𝑡 + 𝑓 ) ) ) , ( 𝑠 ∘ ( 2nd ‘ ( 𝑡 + 𝑓 ) ) ) 〉 ) |
114 |
37 38 112 113
|
syl12anc |
⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑠 ∈ 𝐸 ∧ 𝑡 ∈ ( 𝑇 × 𝐸 ) ∧ 𝑓 ∈ ( 𝑇 × 𝐸 ) ) ) → ( 𝑠 · ( 𝑡 + 𝑓 ) ) = 〈 ( 𝑠 ‘ ( 1st ‘ ( 𝑡 + 𝑓 ) ) ) , ( 𝑠 ∘ ( 2nd ‘ ( 𝑡 + 𝑓 ) ) ) 〉 ) |
115 |
35
|
3adantr3 |
⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑠 ∈ 𝐸 ∧ 𝑡 ∈ ( 𝑇 × 𝐸 ) ∧ 𝑓 ∈ ( 𝑇 × 𝐸 ) ) ) → ( 𝑠 · 𝑡 ) ∈ ( 𝑇 × 𝐸 ) ) |
116 |
2 3 4 5 12
|
dvhvscacl |
⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑠 ∈ 𝐸 ∧ 𝑓 ∈ ( 𝑇 × 𝐸 ) ) ) → ( 𝑠 · 𝑓 ) ∈ ( 𝑇 × 𝐸 ) ) |
117 |
116
|
3adantr2 |
⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑠 ∈ 𝐸 ∧ 𝑡 ∈ ( 𝑇 × 𝐸 ) ∧ 𝑓 ∈ ( 𝑇 × 𝐸 ) ) ) → ( 𝑠 · 𝑓 ) ∈ ( 𝑇 × 𝐸 ) ) |
118 |
2 3 4 5 6 8 7
|
dvhvadd |
⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( ( 𝑠 · 𝑡 ) ∈ ( 𝑇 × 𝐸 ) ∧ ( 𝑠 · 𝑓 ) ∈ ( 𝑇 × 𝐸 ) ) ) → ( ( 𝑠 · 𝑡 ) + ( 𝑠 · 𝑓 ) ) = 〈 ( ( 1st ‘ ( 𝑠 · 𝑡 ) ) ∘ ( 1st ‘ ( 𝑠 · 𝑓 ) ) ) , ( ( 2nd ‘ ( 𝑠 · 𝑡 ) ) ⨣ ( 2nd ‘ ( 𝑠 · 𝑓 ) ) ) 〉 ) |
119 |
37 115 117 118
|
syl12anc |
⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑠 ∈ 𝐸 ∧ 𝑡 ∈ ( 𝑇 × 𝐸 ) ∧ 𝑓 ∈ ( 𝑇 × 𝐸 ) ) ) → ( ( 𝑠 · 𝑡 ) + ( 𝑠 · 𝑓 ) ) = 〈 ( ( 1st ‘ ( 𝑠 · 𝑡 ) ) ∘ ( 1st ‘ ( 𝑠 · 𝑓 ) ) ) , ( ( 2nd ‘ ( 𝑠 · 𝑡 ) ) ⨣ ( 2nd ‘ ( 𝑠 · 𝑓 ) ) ) 〉 ) |
120 |
110 114 119
|
3eqtr4d |
⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑠 ∈ 𝐸 ∧ 𝑡 ∈ ( 𝑇 × 𝐸 ) ∧ 𝑓 ∈ ( 𝑇 × 𝐸 ) ) ) → ( 𝑠 · ( 𝑡 + 𝑓 ) ) = ( ( 𝑠 · 𝑡 ) + ( 𝑠 · 𝑓 ) ) ) |
121 |
|
simpl |
⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑠 ∈ 𝐸 ∧ 𝑡 ∈ 𝐸 ∧ 𝑓 ∈ ( 𝑇 × 𝐸 ) ) ) → ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ) |
122 |
|
simpr1 |
⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑠 ∈ 𝐸 ∧ 𝑡 ∈ 𝐸 ∧ 𝑓 ∈ ( 𝑇 × 𝐸 ) ) ) → 𝑠 ∈ 𝐸 ) |
123 |
|
simpr2 |
⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑠 ∈ 𝐸 ∧ 𝑡 ∈ 𝐸 ∧ 𝑓 ∈ ( 𝑇 × 𝐸 ) ) ) → 𝑡 ∈ 𝐸 ) |
124 |
|
simpr3 |
⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑠 ∈ 𝐸 ∧ 𝑡 ∈ 𝐸 ∧ 𝑓 ∈ ( 𝑇 × 𝐸 ) ) ) → 𝑓 ∈ ( 𝑇 × 𝐸 ) ) |
125 |
124 43
|
syl |
⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑠 ∈ 𝐸 ∧ 𝑡 ∈ 𝐸 ∧ 𝑓 ∈ ( 𝑇 × 𝐸 ) ) ) → ( 1st ‘ 𝑓 ) ∈ 𝑇 ) |
126 |
|
eqid |
⊢ ( +g ‘ ( ( EDRing ‘ 𝐾 ) ‘ 𝑊 ) ) = ( +g ‘ ( ( EDRing ‘ 𝐾 ) ‘ 𝑊 ) ) |
127 |
2 3 4 24 126
|
erngplus2 |
⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑠 ∈ 𝐸 ∧ 𝑡 ∈ 𝐸 ∧ ( 1st ‘ 𝑓 ) ∈ 𝑇 ) ) → ( ( 𝑠 ( +g ‘ ( ( EDRing ‘ 𝐾 ) ‘ 𝑊 ) ) 𝑡 ) ‘ ( 1st ‘ 𝑓 ) ) = ( ( 𝑠 ‘ ( 1st ‘ 𝑓 ) ) ∘ ( 𝑡 ‘ ( 1st ‘ 𝑓 ) ) ) ) |
128 |
121 122 123 125 127
|
syl13anc |
⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑠 ∈ 𝐸 ∧ 𝑡 ∈ 𝐸 ∧ 𝑓 ∈ ( 𝑇 × 𝐸 ) ) ) → ( ( 𝑠 ( +g ‘ ( ( EDRing ‘ 𝐾 ) ‘ 𝑊 ) ) 𝑡 ) ‘ ( 1st ‘ 𝑓 ) ) = ( ( 𝑠 ‘ ( 1st ‘ 𝑓 ) ) ∘ ( 𝑡 ‘ ( 1st ‘ 𝑓 ) ) ) ) |
129 |
25
|
fveq2d |
⊢ ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) → ( +g ‘ 𝐷 ) = ( +g ‘ ( ( EDRing ‘ 𝐾 ) ‘ 𝑊 ) ) ) |
130 |
7 129
|
syl5eq |
⊢ ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) → ⨣ = ( +g ‘ ( ( EDRing ‘ 𝐾 ) ‘ 𝑊 ) ) ) |
131 |
130
|
oveqd |
⊢ ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) → ( 𝑠 ⨣ 𝑡 ) = ( 𝑠 ( +g ‘ ( ( EDRing ‘ 𝐾 ) ‘ 𝑊 ) ) 𝑡 ) ) |
132 |
131
|
fveq1d |
⊢ ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) → ( ( 𝑠 ⨣ 𝑡 ) ‘ ( 1st ‘ 𝑓 ) ) = ( ( 𝑠 ( +g ‘ ( ( EDRing ‘ 𝐾 ) ‘ 𝑊 ) ) 𝑡 ) ‘ ( 1st ‘ 𝑓 ) ) ) |
133 |
132
|
adantr |
⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑠 ∈ 𝐸 ∧ 𝑡 ∈ 𝐸 ∧ 𝑓 ∈ ( 𝑇 × 𝐸 ) ) ) → ( ( 𝑠 ⨣ 𝑡 ) ‘ ( 1st ‘ 𝑓 ) ) = ( ( 𝑠 ( +g ‘ ( ( EDRing ‘ 𝐾 ) ‘ 𝑊 ) ) 𝑡 ) ‘ ( 1st ‘ 𝑓 ) ) ) |
134 |
66
|
3adantr2 |
⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑠 ∈ 𝐸 ∧ 𝑡 ∈ 𝐸 ∧ 𝑓 ∈ ( 𝑇 × 𝐸 ) ) ) → ( 𝑠 · 𝑓 ) = 〈 ( 𝑠 ‘ ( 1st ‘ 𝑓 ) ) , ( 𝑠 ∘ ( 2nd ‘ 𝑓 ) ) 〉 ) |
135 |
134
|
fveq2d |
⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑠 ∈ 𝐸 ∧ 𝑡 ∈ 𝐸 ∧ 𝑓 ∈ ( 𝑇 × 𝐸 ) ) ) → ( 1st ‘ ( 𝑠 · 𝑓 ) ) = ( 1st ‘ 〈 ( 𝑠 ‘ ( 1st ‘ 𝑓 ) ) , ( 𝑠 ∘ ( 2nd ‘ 𝑓 ) ) 〉 ) ) |
136 |
135 72
|
eqtrdi |
⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑠 ∈ 𝐸 ∧ 𝑡 ∈ 𝐸 ∧ 𝑓 ∈ ( 𝑇 × 𝐸 ) ) ) → ( 1st ‘ ( 𝑠 · 𝑓 ) ) = ( 𝑠 ‘ ( 1st ‘ 𝑓 ) ) ) |
137 |
2 3 4 5 12
|
dvhvsca |
⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑡 ∈ 𝐸 ∧ 𝑓 ∈ ( 𝑇 × 𝐸 ) ) ) → ( 𝑡 · 𝑓 ) = 〈 ( 𝑡 ‘ ( 1st ‘ 𝑓 ) ) , ( 𝑡 ∘ ( 2nd ‘ 𝑓 ) ) 〉 ) |
138 |
137
|
3adantr1 |
⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑠 ∈ 𝐸 ∧ 𝑡 ∈ 𝐸 ∧ 𝑓 ∈ ( 𝑇 × 𝐸 ) ) ) → ( 𝑡 · 𝑓 ) = 〈 ( 𝑡 ‘ ( 1st ‘ 𝑓 ) ) , ( 𝑡 ∘ ( 2nd ‘ 𝑓 ) ) 〉 ) |
139 |
138
|
fveq2d |
⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑠 ∈ 𝐸 ∧ 𝑡 ∈ 𝐸 ∧ 𝑓 ∈ ( 𝑇 × 𝐸 ) ) ) → ( 1st ‘ ( 𝑡 · 𝑓 ) ) = ( 1st ‘ 〈 ( 𝑡 ‘ ( 1st ‘ 𝑓 ) ) , ( 𝑡 ∘ ( 2nd ‘ 𝑓 ) ) 〉 ) ) |
140 |
|
fvex |
⊢ ( 𝑡 ‘ ( 1st ‘ 𝑓 ) ) ∈ V |
141 |
|
vex |
⊢ 𝑡 ∈ V |
142 |
141 70
|
coex |
⊢ ( 𝑡 ∘ ( 2nd ‘ 𝑓 ) ) ∈ V |
143 |
140 142
|
op1st |
⊢ ( 1st ‘ 〈 ( 𝑡 ‘ ( 1st ‘ 𝑓 ) ) , ( 𝑡 ∘ ( 2nd ‘ 𝑓 ) ) 〉 ) = ( 𝑡 ‘ ( 1st ‘ 𝑓 ) ) |
144 |
139 143
|
eqtrdi |
⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑠 ∈ 𝐸 ∧ 𝑡 ∈ 𝐸 ∧ 𝑓 ∈ ( 𝑇 × 𝐸 ) ) ) → ( 1st ‘ ( 𝑡 · 𝑓 ) ) = ( 𝑡 ‘ ( 1st ‘ 𝑓 ) ) ) |
145 |
136 144
|
coeq12d |
⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑠 ∈ 𝐸 ∧ 𝑡 ∈ 𝐸 ∧ 𝑓 ∈ ( 𝑇 × 𝐸 ) ) ) → ( ( 1st ‘ ( 𝑠 · 𝑓 ) ) ∘ ( 1st ‘ ( 𝑡 · 𝑓 ) ) ) = ( ( 𝑠 ‘ ( 1st ‘ 𝑓 ) ) ∘ ( 𝑡 ‘ ( 1st ‘ 𝑓 ) ) ) ) |
146 |
128 133 145
|
3eqtr4d |
⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑠 ∈ 𝐸 ∧ 𝑡 ∈ 𝐸 ∧ 𝑓 ∈ ( 𝑇 × 𝐸 ) ) ) → ( ( 𝑠 ⨣ 𝑡 ) ‘ ( 1st ‘ 𝑓 ) ) = ( ( 1st ‘ ( 𝑠 · 𝑓 ) ) ∘ ( 1st ‘ ( 𝑡 · 𝑓 ) ) ) ) |
147 |
33
|
adantr |
⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑠 ∈ 𝐸 ∧ 𝑡 ∈ 𝐸 ∧ 𝑓 ∈ ( 𝑇 × 𝐸 ) ) ) → 𝐷 ∈ Ring ) |
148 |
21
|
adantr |
⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑠 ∈ 𝐸 ∧ 𝑡 ∈ 𝐸 ∧ 𝑓 ∈ ( 𝑇 × 𝐸 ) ) ) → 𝐸 = ( Base ‘ 𝐷 ) ) |
149 |
122 148
|
eleqtrd |
⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑠 ∈ 𝐸 ∧ 𝑡 ∈ 𝐸 ∧ 𝑓 ∈ ( 𝑇 × 𝐸 ) ) ) → 𝑠 ∈ ( Base ‘ 𝐷 ) ) |
150 |
123 148
|
eleqtrd |
⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑠 ∈ 𝐸 ∧ 𝑡 ∈ 𝐸 ∧ 𝑓 ∈ ( 𝑇 × 𝐸 ) ) ) → 𝑡 ∈ ( Base ‘ 𝐷 ) ) |
151 |
124 82
|
syl |
⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑠 ∈ 𝐸 ∧ 𝑡 ∈ 𝐸 ∧ 𝑓 ∈ ( 𝑇 × 𝐸 ) ) ) → ( 2nd ‘ 𝑓 ) ∈ 𝐸 ) |
152 |
151 148
|
eleqtrd |
⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑠 ∈ 𝐸 ∧ 𝑡 ∈ 𝐸 ∧ 𝑓 ∈ ( 𝑇 × 𝐸 ) ) ) → ( 2nd ‘ 𝑓 ) ∈ ( Base ‘ 𝐷 ) ) |
153 |
19 7 11
|
ringdir |
⊢ ( ( 𝐷 ∈ Ring ∧ ( 𝑠 ∈ ( Base ‘ 𝐷 ) ∧ 𝑡 ∈ ( Base ‘ 𝐷 ) ∧ ( 2nd ‘ 𝑓 ) ∈ ( Base ‘ 𝐷 ) ) ) → ( ( 𝑠 ⨣ 𝑡 ) × ( 2nd ‘ 𝑓 ) ) = ( ( 𝑠 × ( 2nd ‘ 𝑓 ) ) ⨣ ( 𝑡 × ( 2nd ‘ 𝑓 ) ) ) ) |
154 |
147 149 150 152 153
|
syl13anc |
⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑠 ∈ 𝐸 ∧ 𝑡 ∈ 𝐸 ∧ 𝑓 ∈ ( 𝑇 × 𝐸 ) ) ) → ( ( 𝑠 ⨣ 𝑡 ) × ( 2nd ‘ 𝑓 ) ) = ( ( 𝑠 × ( 2nd ‘ 𝑓 ) ) ⨣ ( 𝑡 × ( 2nd ‘ 𝑓 ) ) ) ) |
155 |
19 7
|
ringacl |
⊢ ( ( 𝐷 ∈ Ring ∧ 𝑠 ∈ ( Base ‘ 𝐷 ) ∧ 𝑡 ∈ ( Base ‘ 𝐷 ) ) → ( 𝑠 ⨣ 𝑡 ) ∈ ( Base ‘ 𝐷 ) ) |
156 |
147 149 150 155
|
syl3anc |
⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑠 ∈ 𝐸 ∧ 𝑡 ∈ 𝐸 ∧ 𝑓 ∈ ( 𝑇 × 𝐸 ) ) ) → ( 𝑠 ⨣ 𝑡 ) ∈ ( Base ‘ 𝐷 ) ) |
157 |
156 148
|
eleqtrrd |
⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑠 ∈ 𝐸 ∧ 𝑡 ∈ 𝐸 ∧ 𝑓 ∈ ( 𝑇 × 𝐸 ) ) ) → ( 𝑠 ⨣ 𝑡 ) ∈ 𝐸 ) |
158 |
2 3 4 5 6 11
|
dvhmulr |
⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( ( 𝑠 ⨣ 𝑡 ) ∈ 𝐸 ∧ ( 2nd ‘ 𝑓 ) ∈ 𝐸 ) ) → ( ( 𝑠 ⨣ 𝑡 ) × ( 2nd ‘ 𝑓 ) ) = ( ( 𝑠 ⨣ 𝑡 ) ∘ ( 2nd ‘ 𝑓 ) ) ) |
159 |
121 157 151 158
|
syl12anc |
⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑠 ∈ 𝐸 ∧ 𝑡 ∈ 𝐸 ∧ 𝑓 ∈ ( 𝑇 × 𝐸 ) ) ) → ( ( 𝑠 ⨣ 𝑡 ) × ( 2nd ‘ 𝑓 ) ) = ( ( 𝑠 ⨣ 𝑡 ) ∘ ( 2nd ‘ 𝑓 ) ) ) |
160 |
121 122 151 94
|
syl12anc |
⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑠 ∈ 𝐸 ∧ 𝑡 ∈ 𝐸 ∧ 𝑓 ∈ ( 𝑇 × 𝐸 ) ) ) → ( 𝑠 × ( 2nd ‘ 𝑓 ) ) = ( 𝑠 ∘ ( 2nd ‘ 𝑓 ) ) ) |
161 |
2 3 4 5 6 11
|
dvhmulr |
⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑡 ∈ 𝐸 ∧ ( 2nd ‘ 𝑓 ) ∈ 𝐸 ) ) → ( 𝑡 × ( 2nd ‘ 𝑓 ) ) = ( 𝑡 ∘ ( 2nd ‘ 𝑓 ) ) ) |
162 |
121 123 151 161
|
syl12anc |
⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑠 ∈ 𝐸 ∧ 𝑡 ∈ 𝐸 ∧ 𝑓 ∈ ( 𝑇 × 𝐸 ) ) ) → ( 𝑡 × ( 2nd ‘ 𝑓 ) ) = ( 𝑡 ∘ ( 2nd ‘ 𝑓 ) ) ) |
163 |
160 162
|
oveq12d |
⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑠 ∈ 𝐸 ∧ 𝑡 ∈ 𝐸 ∧ 𝑓 ∈ ( 𝑇 × 𝐸 ) ) ) → ( ( 𝑠 × ( 2nd ‘ 𝑓 ) ) ⨣ ( 𝑡 × ( 2nd ‘ 𝑓 ) ) ) = ( ( 𝑠 ∘ ( 2nd ‘ 𝑓 ) ) ⨣ ( 𝑡 ∘ ( 2nd ‘ 𝑓 ) ) ) ) |
164 |
154 159 163
|
3eqtr3d |
⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑠 ∈ 𝐸 ∧ 𝑡 ∈ 𝐸 ∧ 𝑓 ∈ ( 𝑇 × 𝐸 ) ) ) → ( ( 𝑠 ⨣ 𝑡 ) ∘ ( 2nd ‘ 𝑓 ) ) = ( ( 𝑠 ∘ ( 2nd ‘ 𝑓 ) ) ⨣ ( 𝑡 ∘ ( 2nd ‘ 𝑓 ) ) ) ) |
165 |
134
|
fveq2d |
⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑠 ∈ 𝐸 ∧ 𝑡 ∈ 𝐸 ∧ 𝑓 ∈ ( 𝑇 × 𝐸 ) ) ) → ( 2nd ‘ ( 𝑠 · 𝑓 ) ) = ( 2nd ‘ 〈 ( 𝑠 ‘ ( 1st ‘ 𝑓 ) ) , ( 𝑠 ∘ ( 2nd ‘ 𝑓 ) ) 〉 ) ) |
166 |
165 106
|
eqtrdi |
⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑠 ∈ 𝐸 ∧ 𝑡 ∈ 𝐸 ∧ 𝑓 ∈ ( 𝑇 × 𝐸 ) ) ) → ( 2nd ‘ ( 𝑠 · 𝑓 ) ) = ( 𝑠 ∘ ( 2nd ‘ 𝑓 ) ) ) |
167 |
138
|
fveq2d |
⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑠 ∈ 𝐸 ∧ 𝑡 ∈ 𝐸 ∧ 𝑓 ∈ ( 𝑇 × 𝐸 ) ) ) → ( 2nd ‘ ( 𝑡 · 𝑓 ) ) = ( 2nd ‘ 〈 ( 𝑡 ‘ ( 1st ‘ 𝑓 ) ) , ( 𝑡 ∘ ( 2nd ‘ 𝑓 ) ) 〉 ) ) |
168 |
140 142
|
op2nd |
⊢ ( 2nd ‘ 〈 ( 𝑡 ‘ ( 1st ‘ 𝑓 ) ) , ( 𝑡 ∘ ( 2nd ‘ 𝑓 ) ) 〉 ) = ( 𝑡 ∘ ( 2nd ‘ 𝑓 ) ) |
169 |
167 168
|
eqtrdi |
⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑠 ∈ 𝐸 ∧ 𝑡 ∈ 𝐸 ∧ 𝑓 ∈ ( 𝑇 × 𝐸 ) ) ) → ( 2nd ‘ ( 𝑡 · 𝑓 ) ) = ( 𝑡 ∘ ( 2nd ‘ 𝑓 ) ) ) |
170 |
166 169
|
oveq12d |
⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑠 ∈ 𝐸 ∧ 𝑡 ∈ 𝐸 ∧ 𝑓 ∈ ( 𝑇 × 𝐸 ) ) ) → ( ( 2nd ‘ ( 𝑠 · 𝑓 ) ) ⨣ ( 2nd ‘ ( 𝑡 · 𝑓 ) ) ) = ( ( 𝑠 ∘ ( 2nd ‘ 𝑓 ) ) ⨣ ( 𝑡 ∘ ( 2nd ‘ 𝑓 ) ) ) ) |
171 |
164 170
|
eqtr4d |
⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑠 ∈ 𝐸 ∧ 𝑡 ∈ 𝐸 ∧ 𝑓 ∈ ( 𝑇 × 𝐸 ) ) ) → ( ( 𝑠 ⨣ 𝑡 ) ∘ ( 2nd ‘ 𝑓 ) ) = ( ( 2nd ‘ ( 𝑠 · 𝑓 ) ) ⨣ ( 2nd ‘ ( 𝑡 · 𝑓 ) ) ) ) |
172 |
146 171
|
opeq12d |
⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑠 ∈ 𝐸 ∧ 𝑡 ∈ 𝐸 ∧ 𝑓 ∈ ( 𝑇 × 𝐸 ) ) ) → 〈 ( ( 𝑠 ⨣ 𝑡 ) ‘ ( 1st ‘ 𝑓 ) ) , ( ( 𝑠 ⨣ 𝑡 ) ∘ ( 2nd ‘ 𝑓 ) ) 〉 = 〈 ( ( 1st ‘ ( 𝑠 · 𝑓 ) ) ∘ ( 1st ‘ ( 𝑡 · 𝑓 ) ) ) , ( ( 2nd ‘ ( 𝑠 · 𝑓 ) ) ⨣ ( 2nd ‘ ( 𝑡 · 𝑓 ) ) ) 〉 ) |
173 |
2 3 4 5 12
|
dvhvsca |
⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( ( 𝑠 ⨣ 𝑡 ) ∈ 𝐸 ∧ 𝑓 ∈ ( 𝑇 × 𝐸 ) ) ) → ( ( 𝑠 ⨣ 𝑡 ) · 𝑓 ) = 〈 ( ( 𝑠 ⨣ 𝑡 ) ‘ ( 1st ‘ 𝑓 ) ) , ( ( 𝑠 ⨣ 𝑡 ) ∘ ( 2nd ‘ 𝑓 ) ) 〉 ) |
174 |
121 157 124 173
|
syl12anc |
⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑠 ∈ 𝐸 ∧ 𝑡 ∈ 𝐸 ∧ 𝑓 ∈ ( 𝑇 × 𝐸 ) ) ) → ( ( 𝑠 ⨣ 𝑡 ) · 𝑓 ) = 〈 ( ( 𝑠 ⨣ 𝑡 ) ‘ ( 1st ‘ 𝑓 ) ) , ( ( 𝑠 ⨣ 𝑡 ) ∘ ( 2nd ‘ 𝑓 ) ) 〉 ) |
175 |
116
|
3adantr2 |
⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑠 ∈ 𝐸 ∧ 𝑡 ∈ 𝐸 ∧ 𝑓 ∈ ( 𝑇 × 𝐸 ) ) ) → ( 𝑠 · 𝑓 ) ∈ ( 𝑇 × 𝐸 ) ) |
176 |
2 3 4 5 12
|
dvhvscacl |
⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑡 ∈ 𝐸 ∧ 𝑓 ∈ ( 𝑇 × 𝐸 ) ) ) → ( 𝑡 · 𝑓 ) ∈ ( 𝑇 × 𝐸 ) ) |
177 |
176
|
3adantr1 |
⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑠 ∈ 𝐸 ∧ 𝑡 ∈ 𝐸 ∧ 𝑓 ∈ ( 𝑇 × 𝐸 ) ) ) → ( 𝑡 · 𝑓 ) ∈ ( 𝑇 × 𝐸 ) ) |
178 |
2 3 4 5 6 8 7
|
dvhvadd |
⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( ( 𝑠 · 𝑓 ) ∈ ( 𝑇 × 𝐸 ) ∧ ( 𝑡 · 𝑓 ) ∈ ( 𝑇 × 𝐸 ) ) ) → ( ( 𝑠 · 𝑓 ) + ( 𝑡 · 𝑓 ) ) = 〈 ( ( 1st ‘ ( 𝑠 · 𝑓 ) ) ∘ ( 1st ‘ ( 𝑡 · 𝑓 ) ) ) , ( ( 2nd ‘ ( 𝑠 · 𝑓 ) ) ⨣ ( 2nd ‘ ( 𝑡 · 𝑓 ) ) ) 〉 ) |
179 |
121 175 177 178
|
syl12anc |
⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑠 ∈ 𝐸 ∧ 𝑡 ∈ 𝐸 ∧ 𝑓 ∈ ( 𝑇 × 𝐸 ) ) ) → ( ( 𝑠 · 𝑓 ) + ( 𝑡 · 𝑓 ) ) = 〈 ( ( 1st ‘ ( 𝑠 · 𝑓 ) ) ∘ ( 1st ‘ ( 𝑡 · 𝑓 ) ) ) , ( ( 2nd ‘ ( 𝑠 · 𝑓 ) ) ⨣ ( 2nd ‘ ( 𝑡 · 𝑓 ) ) ) 〉 ) |
180 |
172 174 179
|
3eqtr4d |
⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑠 ∈ 𝐸 ∧ 𝑡 ∈ 𝐸 ∧ 𝑓 ∈ ( 𝑇 × 𝐸 ) ) ) → ( ( 𝑠 ⨣ 𝑡 ) · 𝑓 ) = ( ( 𝑠 · 𝑓 ) + ( 𝑡 · 𝑓 ) ) ) |
181 |
2 3 4
|
tendocoval |
⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑠 ∈ 𝐸 ∧ 𝑡 ∈ 𝐸 ) ∧ ( 1st ‘ 𝑓 ) ∈ 𝑇 ) → ( ( 𝑠 ∘ 𝑡 ) ‘ ( 1st ‘ 𝑓 ) ) = ( 𝑠 ‘ ( 𝑡 ‘ ( 1st ‘ 𝑓 ) ) ) ) |
182 |
121 122 123 125 181
|
syl121anc |
⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑠 ∈ 𝐸 ∧ 𝑡 ∈ 𝐸 ∧ 𝑓 ∈ ( 𝑇 × 𝐸 ) ) ) → ( ( 𝑠 ∘ 𝑡 ) ‘ ( 1st ‘ 𝑓 ) ) = ( 𝑠 ‘ ( 𝑡 ‘ ( 1st ‘ 𝑓 ) ) ) ) |
183 |
|
coass |
⊢ ( ( 𝑠 ∘ 𝑡 ) ∘ ( 2nd ‘ 𝑓 ) ) = ( 𝑠 ∘ ( 𝑡 ∘ ( 2nd ‘ 𝑓 ) ) ) |
184 |
183
|
a1i |
⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑠 ∈ 𝐸 ∧ 𝑡 ∈ 𝐸 ∧ 𝑓 ∈ ( 𝑇 × 𝐸 ) ) ) → ( ( 𝑠 ∘ 𝑡 ) ∘ ( 2nd ‘ 𝑓 ) ) = ( 𝑠 ∘ ( 𝑡 ∘ ( 2nd ‘ 𝑓 ) ) ) ) |
185 |
182 184
|
opeq12d |
⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑠 ∈ 𝐸 ∧ 𝑡 ∈ 𝐸 ∧ 𝑓 ∈ ( 𝑇 × 𝐸 ) ) ) → 〈 ( ( 𝑠 ∘ 𝑡 ) ‘ ( 1st ‘ 𝑓 ) ) , ( ( 𝑠 ∘ 𝑡 ) ∘ ( 2nd ‘ 𝑓 ) ) 〉 = 〈 ( 𝑠 ‘ ( 𝑡 ‘ ( 1st ‘ 𝑓 ) ) ) , ( 𝑠 ∘ ( 𝑡 ∘ ( 2nd ‘ 𝑓 ) ) ) 〉 ) |
186 |
2 4
|
tendococl |
⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑠 ∈ 𝐸 ∧ 𝑡 ∈ 𝐸 ) → ( 𝑠 ∘ 𝑡 ) ∈ 𝐸 ) |
187 |
121 122 123 186
|
syl3anc |
⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑠 ∈ 𝐸 ∧ 𝑡 ∈ 𝐸 ∧ 𝑓 ∈ ( 𝑇 × 𝐸 ) ) ) → ( 𝑠 ∘ 𝑡 ) ∈ 𝐸 ) |
188 |
2 3 4 5 12
|
dvhvsca |
⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( ( 𝑠 ∘ 𝑡 ) ∈ 𝐸 ∧ 𝑓 ∈ ( 𝑇 × 𝐸 ) ) ) → ( ( 𝑠 ∘ 𝑡 ) · 𝑓 ) = 〈 ( ( 𝑠 ∘ 𝑡 ) ‘ ( 1st ‘ 𝑓 ) ) , ( ( 𝑠 ∘ 𝑡 ) ∘ ( 2nd ‘ 𝑓 ) ) 〉 ) |
189 |
121 187 124 188
|
syl12anc |
⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑠 ∈ 𝐸 ∧ 𝑡 ∈ 𝐸 ∧ 𝑓 ∈ ( 𝑇 × 𝐸 ) ) ) → ( ( 𝑠 ∘ 𝑡 ) · 𝑓 ) = 〈 ( ( 𝑠 ∘ 𝑡 ) ‘ ( 1st ‘ 𝑓 ) ) , ( ( 𝑠 ∘ 𝑡 ) ∘ ( 2nd ‘ 𝑓 ) ) 〉 ) |
190 |
2 3 4
|
tendocl |
⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑡 ∈ 𝐸 ∧ ( 1st ‘ 𝑓 ) ∈ 𝑇 ) → ( 𝑡 ‘ ( 1st ‘ 𝑓 ) ) ∈ 𝑇 ) |
191 |
121 123 125 190
|
syl3anc |
⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑠 ∈ 𝐸 ∧ 𝑡 ∈ 𝐸 ∧ 𝑓 ∈ ( 𝑇 × 𝐸 ) ) ) → ( 𝑡 ‘ ( 1st ‘ 𝑓 ) ) ∈ 𝑇 ) |
192 |
2 4
|
tendococl |
⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑡 ∈ 𝐸 ∧ ( 2nd ‘ 𝑓 ) ∈ 𝐸 ) → ( 𝑡 ∘ ( 2nd ‘ 𝑓 ) ) ∈ 𝐸 ) |
193 |
121 123 151 192
|
syl3anc |
⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑠 ∈ 𝐸 ∧ 𝑡 ∈ 𝐸 ∧ 𝑓 ∈ ( 𝑇 × 𝐸 ) ) ) → ( 𝑡 ∘ ( 2nd ‘ 𝑓 ) ) ∈ 𝐸 ) |
194 |
2 3 4 5 12
|
dvhopvsca |
⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑠 ∈ 𝐸 ∧ ( 𝑡 ‘ ( 1st ‘ 𝑓 ) ) ∈ 𝑇 ∧ ( 𝑡 ∘ ( 2nd ‘ 𝑓 ) ) ∈ 𝐸 ) ) → ( 𝑠 · 〈 ( 𝑡 ‘ ( 1st ‘ 𝑓 ) ) , ( 𝑡 ∘ ( 2nd ‘ 𝑓 ) ) 〉 ) = 〈 ( 𝑠 ‘ ( 𝑡 ‘ ( 1st ‘ 𝑓 ) ) ) , ( 𝑠 ∘ ( 𝑡 ∘ ( 2nd ‘ 𝑓 ) ) ) 〉 ) |
195 |
121 122 191 193 194
|
syl13anc |
⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑠 ∈ 𝐸 ∧ 𝑡 ∈ 𝐸 ∧ 𝑓 ∈ ( 𝑇 × 𝐸 ) ) ) → ( 𝑠 · 〈 ( 𝑡 ‘ ( 1st ‘ 𝑓 ) ) , ( 𝑡 ∘ ( 2nd ‘ 𝑓 ) ) 〉 ) = 〈 ( 𝑠 ‘ ( 𝑡 ‘ ( 1st ‘ 𝑓 ) ) ) , ( 𝑠 ∘ ( 𝑡 ∘ ( 2nd ‘ 𝑓 ) ) ) 〉 ) |
196 |
185 189 195
|
3eqtr4d |
⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑠 ∈ 𝐸 ∧ 𝑡 ∈ 𝐸 ∧ 𝑓 ∈ ( 𝑇 × 𝐸 ) ) ) → ( ( 𝑠 ∘ 𝑡 ) · 𝑓 ) = ( 𝑠 · 〈 ( 𝑡 ‘ ( 1st ‘ 𝑓 ) ) , ( 𝑡 ∘ ( 2nd ‘ 𝑓 ) ) 〉 ) ) |
197 |
2 3 4 5 6 11
|
dvhmulr |
⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑠 ∈ 𝐸 ∧ 𝑡 ∈ 𝐸 ) ) → ( 𝑠 × 𝑡 ) = ( 𝑠 ∘ 𝑡 ) ) |
198 |
197
|
3adantr3 |
⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑠 ∈ 𝐸 ∧ 𝑡 ∈ 𝐸 ∧ 𝑓 ∈ ( 𝑇 × 𝐸 ) ) ) → ( 𝑠 × 𝑡 ) = ( 𝑠 ∘ 𝑡 ) ) |
199 |
198
|
oveq1d |
⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑠 ∈ 𝐸 ∧ 𝑡 ∈ 𝐸 ∧ 𝑓 ∈ ( 𝑇 × 𝐸 ) ) ) → ( ( 𝑠 × 𝑡 ) · 𝑓 ) = ( ( 𝑠 ∘ 𝑡 ) · 𝑓 ) ) |
200 |
138
|
oveq2d |
⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑠 ∈ 𝐸 ∧ 𝑡 ∈ 𝐸 ∧ 𝑓 ∈ ( 𝑇 × 𝐸 ) ) ) → ( 𝑠 · ( 𝑡 · 𝑓 ) ) = ( 𝑠 · 〈 ( 𝑡 ‘ ( 1st ‘ 𝑓 ) ) , ( 𝑡 ∘ ( 2nd ‘ 𝑓 ) ) 〉 ) ) |
201 |
196 199 200
|
3eqtr4d |
⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑠 ∈ 𝐸 ∧ 𝑡 ∈ 𝐸 ∧ 𝑓 ∈ ( 𝑇 × 𝐸 ) ) ) → ( ( 𝑠 × 𝑡 ) · 𝑓 ) = ( 𝑠 · ( 𝑡 · 𝑓 ) ) ) |
202 |
|
xp1st |
⊢ ( 𝑠 ∈ ( 𝑇 × 𝐸 ) → ( 1st ‘ 𝑠 ) ∈ 𝑇 ) |
203 |
202
|
adantl |
⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑠 ∈ ( 𝑇 × 𝐸 ) ) → ( 1st ‘ 𝑠 ) ∈ 𝑇 ) |
204 |
|
fvresi |
⊢ ( ( 1st ‘ 𝑠 ) ∈ 𝑇 → ( ( I ↾ 𝑇 ) ‘ ( 1st ‘ 𝑠 ) ) = ( 1st ‘ 𝑠 ) ) |
205 |
203 204
|
syl |
⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑠 ∈ ( 𝑇 × 𝐸 ) ) → ( ( I ↾ 𝑇 ) ‘ ( 1st ‘ 𝑠 ) ) = ( 1st ‘ 𝑠 ) ) |
206 |
|
xp2nd |
⊢ ( 𝑠 ∈ ( 𝑇 × 𝐸 ) → ( 2nd ‘ 𝑠 ) ∈ 𝐸 ) |
207 |
2 3 4
|
tendof |
⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 2nd ‘ 𝑠 ) ∈ 𝐸 ) → ( 2nd ‘ 𝑠 ) : 𝑇 ⟶ 𝑇 ) |
208 |
206 207
|
sylan2 |
⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑠 ∈ ( 𝑇 × 𝐸 ) ) → ( 2nd ‘ 𝑠 ) : 𝑇 ⟶ 𝑇 ) |
209 |
|
fcoi2 |
⊢ ( ( 2nd ‘ 𝑠 ) : 𝑇 ⟶ 𝑇 → ( ( I ↾ 𝑇 ) ∘ ( 2nd ‘ 𝑠 ) ) = ( 2nd ‘ 𝑠 ) ) |
210 |
208 209
|
syl |
⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑠 ∈ ( 𝑇 × 𝐸 ) ) → ( ( I ↾ 𝑇 ) ∘ ( 2nd ‘ 𝑠 ) ) = ( 2nd ‘ 𝑠 ) ) |
211 |
205 210
|
opeq12d |
⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑠 ∈ ( 𝑇 × 𝐸 ) ) → 〈 ( ( I ↾ 𝑇 ) ‘ ( 1st ‘ 𝑠 ) ) , ( ( I ↾ 𝑇 ) ∘ ( 2nd ‘ 𝑠 ) ) 〉 = 〈 ( 1st ‘ 𝑠 ) , ( 2nd ‘ 𝑠 ) 〉 ) |
212 |
2 3 4
|
tendoidcl |
⊢ ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) → ( I ↾ 𝑇 ) ∈ 𝐸 ) |
213 |
212
|
anim1i |
⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑠 ∈ ( 𝑇 × 𝐸 ) ) → ( ( I ↾ 𝑇 ) ∈ 𝐸 ∧ 𝑠 ∈ ( 𝑇 × 𝐸 ) ) ) |
214 |
2 3 4 5 12
|
dvhvsca |
⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( ( I ↾ 𝑇 ) ∈ 𝐸 ∧ 𝑠 ∈ ( 𝑇 × 𝐸 ) ) ) → ( ( I ↾ 𝑇 ) · 𝑠 ) = 〈 ( ( I ↾ 𝑇 ) ‘ ( 1st ‘ 𝑠 ) ) , ( ( I ↾ 𝑇 ) ∘ ( 2nd ‘ 𝑠 ) ) 〉 ) |
215 |
213 214
|
syldan |
⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑠 ∈ ( 𝑇 × 𝐸 ) ) → ( ( I ↾ 𝑇 ) · 𝑠 ) = 〈 ( ( I ↾ 𝑇 ) ‘ ( 1st ‘ 𝑠 ) ) , ( ( I ↾ 𝑇 ) ∘ ( 2nd ‘ 𝑠 ) ) 〉 ) |
216 |
|
1st2nd2 |
⊢ ( 𝑠 ∈ ( 𝑇 × 𝐸 ) → 𝑠 = 〈 ( 1st ‘ 𝑠 ) , ( 2nd ‘ 𝑠 ) 〉 ) |
217 |
216
|
adantl |
⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑠 ∈ ( 𝑇 × 𝐸 ) ) → 𝑠 = 〈 ( 1st ‘ 𝑠 ) , ( 2nd ‘ 𝑠 ) 〉 ) |
218 |
211 215 217
|
3eqtr4d |
⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑠 ∈ ( 𝑇 × 𝐸 ) ) → ( ( I ↾ 𝑇 ) · 𝑠 ) = 𝑠 ) |
219 |
15 16 17 18 21 22 23 29 33 34 36 120 180 201 218
|
islmodd |
⊢ ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) → 𝑈 ∈ LMod ) |
220 |
6
|
islvec |
⊢ ( 𝑈 ∈ LVec ↔ ( 𝑈 ∈ LMod ∧ 𝐷 ∈ DivRing ) ) |
221 |
219 31 220
|
sylanbrc |
⊢ ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) → 𝑈 ∈ LVec ) |