Step |
Hyp |
Ref |
Expression |
1 |
|
isslmd.v |
⊢ 𝑉 = ( Base ‘ 𝑊 ) |
2 |
|
isslmd.a |
⊢ + = ( +g ‘ 𝑊 ) |
3 |
|
isslmd.s |
⊢ · = ( ·𝑠 ‘ 𝑊 ) |
4 |
|
isslmd.0 |
⊢ 0 = ( 0g ‘ 𝑊 ) |
5 |
|
isslmd.f |
⊢ 𝐹 = ( Scalar ‘ 𝑊 ) |
6 |
|
isslmd.k |
⊢ 𝐾 = ( Base ‘ 𝐹 ) |
7 |
|
isslmd.p |
⊢ ⨣ = ( +g ‘ 𝐹 ) |
8 |
|
isslmd.t |
⊢ × = ( .r ‘ 𝐹 ) |
9 |
|
isslmd.u |
⊢ 1 = ( 1r ‘ 𝐹 ) |
10 |
|
isslmd.o |
⊢ 𝑂 = ( 0g ‘ 𝐹 ) |
11 |
|
fvex |
⊢ ( Base ‘ 𝑔 ) ∈ V |
12 |
|
fvex |
⊢ ( +g ‘ 𝑔 ) ∈ V |
13 |
|
fvex |
⊢ ( ·𝑠 ‘ 𝑔 ) ∈ V |
14 |
|
fvex |
⊢ ( Scalar ‘ 𝑔 ) ∈ V |
15 |
|
fvex |
⊢ ( Base ‘ 𝑓 ) ∈ V |
16 |
|
fvex |
⊢ ( +g ‘ 𝑓 ) ∈ V |
17 |
|
fvex |
⊢ ( .r ‘ 𝑓 ) ∈ V |
18 |
|
simp1 |
⊢ ( ( 𝑘 = ( Base ‘ 𝑓 ) ∧ 𝑝 = ( +g ‘ 𝑓 ) ∧ 𝑡 = ( .r ‘ 𝑓 ) ) → 𝑘 = ( Base ‘ 𝑓 ) ) |
19 |
|
simp2 |
⊢ ( ( 𝑘 = ( Base ‘ 𝑓 ) ∧ 𝑝 = ( +g ‘ 𝑓 ) ∧ 𝑡 = ( .r ‘ 𝑓 ) ) → 𝑝 = ( +g ‘ 𝑓 ) ) |
20 |
19
|
oveqd |
⊢ ( ( 𝑘 = ( Base ‘ 𝑓 ) ∧ 𝑝 = ( +g ‘ 𝑓 ) ∧ 𝑡 = ( .r ‘ 𝑓 ) ) → ( 𝑞 𝑝 𝑟 ) = ( 𝑞 ( +g ‘ 𝑓 ) 𝑟 ) ) |
21 |
20
|
oveq1d |
⊢ ( ( 𝑘 = ( Base ‘ 𝑓 ) ∧ 𝑝 = ( +g ‘ 𝑓 ) ∧ 𝑡 = ( .r ‘ 𝑓 ) ) → ( ( 𝑞 𝑝 𝑟 ) 𝑠 𝑤 ) = ( ( 𝑞 ( +g ‘ 𝑓 ) 𝑟 ) 𝑠 𝑤 ) ) |
22 |
21
|
eqeq1d |
⊢ ( ( 𝑘 = ( Base ‘ 𝑓 ) ∧ 𝑝 = ( +g ‘ 𝑓 ) ∧ 𝑡 = ( .r ‘ 𝑓 ) ) → ( ( ( 𝑞 𝑝 𝑟 ) 𝑠 𝑤 ) = ( ( 𝑞 𝑠 𝑤 ) 𝑎 ( 𝑟 𝑠 𝑤 ) ) ↔ ( ( 𝑞 ( +g ‘ 𝑓 ) 𝑟 ) 𝑠 𝑤 ) = ( ( 𝑞 𝑠 𝑤 ) 𝑎 ( 𝑟 𝑠 𝑤 ) ) ) ) |
23 |
22
|
3anbi3d |
⊢ ( ( 𝑘 = ( Base ‘ 𝑓 ) ∧ 𝑝 = ( +g ‘ 𝑓 ) ∧ 𝑡 = ( .r ‘ 𝑓 ) ) → ( ( ( 𝑟 𝑠 𝑤 ) ∈ 𝑣 ∧ ( 𝑟 𝑠 ( 𝑤 𝑎 𝑥 ) ) = ( ( 𝑟 𝑠 𝑤 ) 𝑎 ( 𝑟 𝑠 𝑥 ) ) ∧ ( ( 𝑞 𝑝 𝑟 ) 𝑠 𝑤 ) = ( ( 𝑞 𝑠 𝑤 ) 𝑎 ( 𝑟 𝑠 𝑤 ) ) ) ↔ ( ( 𝑟 𝑠 𝑤 ) ∈ 𝑣 ∧ ( 𝑟 𝑠 ( 𝑤 𝑎 𝑥 ) ) = ( ( 𝑟 𝑠 𝑤 ) 𝑎 ( 𝑟 𝑠 𝑥 ) ) ∧ ( ( 𝑞 ( +g ‘ 𝑓 ) 𝑟 ) 𝑠 𝑤 ) = ( ( 𝑞 𝑠 𝑤 ) 𝑎 ( 𝑟 𝑠 𝑤 ) ) ) ) ) |
24 |
|
simp3 |
⊢ ( ( 𝑘 = ( Base ‘ 𝑓 ) ∧ 𝑝 = ( +g ‘ 𝑓 ) ∧ 𝑡 = ( .r ‘ 𝑓 ) ) → 𝑡 = ( .r ‘ 𝑓 ) ) |
25 |
24
|
oveqd |
⊢ ( ( 𝑘 = ( Base ‘ 𝑓 ) ∧ 𝑝 = ( +g ‘ 𝑓 ) ∧ 𝑡 = ( .r ‘ 𝑓 ) ) → ( 𝑞 𝑡 𝑟 ) = ( 𝑞 ( .r ‘ 𝑓 ) 𝑟 ) ) |
26 |
25
|
oveq1d |
⊢ ( ( 𝑘 = ( Base ‘ 𝑓 ) ∧ 𝑝 = ( +g ‘ 𝑓 ) ∧ 𝑡 = ( .r ‘ 𝑓 ) ) → ( ( 𝑞 𝑡 𝑟 ) 𝑠 𝑤 ) = ( ( 𝑞 ( .r ‘ 𝑓 ) 𝑟 ) 𝑠 𝑤 ) ) |
27 |
26
|
eqeq1d |
⊢ ( ( 𝑘 = ( Base ‘ 𝑓 ) ∧ 𝑝 = ( +g ‘ 𝑓 ) ∧ 𝑡 = ( .r ‘ 𝑓 ) ) → ( ( ( 𝑞 𝑡 𝑟 ) 𝑠 𝑤 ) = ( 𝑞 𝑠 ( 𝑟 𝑠 𝑤 ) ) ↔ ( ( 𝑞 ( .r ‘ 𝑓 ) 𝑟 ) 𝑠 𝑤 ) = ( 𝑞 𝑠 ( 𝑟 𝑠 𝑤 ) ) ) ) |
28 |
27
|
3anbi1d |
⊢ ( ( 𝑘 = ( Base ‘ 𝑓 ) ∧ 𝑝 = ( +g ‘ 𝑓 ) ∧ 𝑡 = ( .r ‘ 𝑓 ) ) → ( ( ( ( 𝑞 𝑡 𝑟 ) 𝑠 𝑤 ) = ( 𝑞 𝑠 ( 𝑟 𝑠 𝑤 ) ) ∧ ( ( 1r ‘ 𝑓 ) 𝑠 𝑤 ) = 𝑤 ∧ ( ( 0g ‘ 𝑓 ) 𝑠 𝑤 ) = ( 0g ‘ 𝑔 ) ) ↔ ( ( ( 𝑞 ( .r ‘ 𝑓 ) 𝑟 ) 𝑠 𝑤 ) = ( 𝑞 𝑠 ( 𝑟 𝑠 𝑤 ) ) ∧ ( ( 1r ‘ 𝑓 ) 𝑠 𝑤 ) = 𝑤 ∧ ( ( 0g ‘ 𝑓 ) 𝑠 𝑤 ) = ( 0g ‘ 𝑔 ) ) ) ) |
29 |
23 28
|
anbi12d |
⊢ ( ( 𝑘 = ( Base ‘ 𝑓 ) ∧ 𝑝 = ( +g ‘ 𝑓 ) ∧ 𝑡 = ( .r ‘ 𝑓 ) ) → ( ( ( ( 𝑟 𝑠 𝑤 ) ∈ 𝑣 ∧ ( 𝑟 𝑠 ( 𝑤 𝑎 𝑥 ) ) = ( ( 𝑟 𝑠 𝑤 ) 𝑎 ( 𝑟 𝑠 𝑥 ) ) ∧ ( ( 𝑞 𝑝 𝑟 ) 𝑠 𝑤 ) = ( ( 𝑞 𝑠 𝑤 ) 𝑎 ( 𝑟 𝑠 𝑤 ) ) ) ∧ ( ( ( 𝑞 𝑡 𝑟 ) 𝑠 𝑤 ) = ( 𝑞 𝑠 ( 𝑟 𝑠 𝑤 ) ) ∧ ( ( 1r ‘ 𝑓 ) 𝑠 𝑤 ) = 𝑤 ∧ ( ( 0g ‘ 𝑓 ) 𝑠 𝑤 ) = ( 0g ‘ 𝑔 ) ) ) ↔ ( ( ( 𝑟 𝑠 𝑤 ) ∈ 𝑣 ∧ ( 𝑟 𝑠 ( 𝑤 𝑎 𝑥 ) ) = ( ( 𝑟 𝑠 𝑤 ) 𝑎 ( 𝑟 𝑠 𝑥 ) ) ∧ ( ( 𝑞 ( +g ‘ 𝑓 ) 𝑟 ) 𝑠 𝑤 ) = ( ( 𝑞 𝑠 𝑤 ) 𝑎 ( 𝑟 𝑠 𝑤 ) ) ) ∧ ( ( ( 𝑞 ( .r ‘ 𝑓 ) 𝑟 ) 𝑠 𝑤 ) = ( 𝑞 𝑠 ( 𝑟 𝑠 𝑤 ) ) ∧ ( ( 1r ‘ 𝑓 ) 𝑠 𝑤 ) = 𝑤 ∧ ( ( 0g ‘ 𝑓 ) 𝑠 𝑤 ) = ( 0g ‘ 𝑔 ) ) ) ) ) |
30 |
29
|
2ralbidv |
⊢ ( ( 𝑘 = ( Base ‘ 𝑓 ) ∧ 𝑝 = ( +g ‘ 𝑓 ) ∧ 𝑡 = ( .r ‘ 𝑓 ) ) → ( ∀ 𝑥 ∈ 𝑣 ∀ 𝑤 ∈ 𝑣 ( ( ( 𝑟 𝑠 𝑤 ) ∈ 𝑣 ∧ ( 𝑟 𝑠 ( 𝑤 𝑎 𝑥 ) ) = ( ( 𝑟 𝑠 𝑤 ) 𝑎 ( 𝑟 𝑠 𝑥 ) ) ∧ ( ( 𝑞 𝑝 𝑟 ) 𝑠 𝑤 ) = ( ( 𝑞 𝑠 𝑤 ) 𝑎 ( 𝑟 𝑠 𝑤 ) ) ) ∧ ( ( ( 𝑞 𝑡 𝑟 ) 𝑠 𝑤 ) = ( 𝑞 𝑠 ( 𝑟 𝑠 𝑤 ) ) ∧ ( ( 1r ‘ 𝑓 ) 𝑠 𝑤 ) = 𝑤 ∧ ( ( 0g ‘ 𝑓 ) 𝑠 𝑤 ) = ( 0g ‘ 𝑔 ) ) ) ↔ ∀ 𝑥 ∈ 𝑣 ∀ 𝑤 ∈ 𝑣 ( ( ( 𝑟 𝑠 𝑤 ) ∈ 𝑣 ∧ ( 𝑟 𝑠 ( 𝑤 𝑎 𝑥 ) ) = ( ( 𝑟 𝑠 𝑤 ) 𝑎 ( 𝑟 𝑠 𝑥 ) ) ∧ ( ( 𝑞 ( +g ‘ 𝑓 ) 𝑟 ) 𝑠 𝑤 ) = ( ( 𝑞 𝑠 𝑤 ) 𝑎 ( 𝑟 𝑠 𝑤 ) ) ) ∧ ( ( ( 𝑞 ( .r ‘ 𝑓 ) 𝑟 ) 𝑠 𝑤 ) = ( 𝑞 𝑠 ( 𝑟 𝑠 𝑤 ) ) ∧ ( ( 1r ‘ 𝑓 ) 𝑠 𝑤 ) = 𝑤 ∧ ( ( 0g ‘ 𝑓 ) 𝑠 𝑤 ) = ( 0g ‘ 𝑔 ) ) ) ) ) |
31 |
18 30
|
raleqbidv |
⊢ ( ( 𝑘 = ( Base ‘ 𝑓 ) ∧ 𝑝 = ( +g ‘ 𝑓 ) ∧ 𝑡 = ( .r ‘ 𝑓 ) ) → ( ∀ 𝑟 ∈ 𝑘 ∀ 𝑥 ∈ 𝑣 ∀ 𝑤 ∈ 𝑣 ( ( ( 𝑟 𝑠 𝑤 ) ∈ 𝑣 ∧ ( 𝑟 𝑠 ( 𝑤 𝑎 𝑥 ) ) = ( ( 𝑟 𝑠 𝑤 ) 𝑎 ( 𝑟 𝑠 𝑥 ) ) ∧ ( ( 𝑞 𝑝 𝑟 ) 𝑠 𝑤 ) = ( ( 𝑞 𝑠 𝑤 ) 𝑎 ( 𝑟 𝑠 𝑤 ) ) ) ∧ ( ( ( 𝑞 𝑡 𝑟 ) 𝑠 𝑤 ) = ( 𝑞 𝑠 ( 𝑟 𝑠 𝑤 ) ) ∧ ( ( 1r ‘ 𝑓 ) 𝑠 𝑤 ) = 𝑤 ∧ ( ( 0g ‘ 𝑓 ) 𝑠 𝑤 ) = ( 0g ‘ 𝑔 ) ) ) ↔ ∀ 𝑟 ∈ ( Base ‘ 𝑓 ) ∀ 𝑥 ∈ 𝑣 ∀ 𝑤 ∈ 𝑣 ( ( ( 𝑟 𝑠 𝑤 ) ∈ 𝑣 ∧ ( 𝑟 𝑠 ( 𝑤 𝑎 𝑥 ) ) = ( ( 𝑟 𝑠 𝑤 ) 𝑎 ( 𝑟 𝑠 𝑥 ) ) ∧ ( ( 𝑞 ( +g ‘ 𝑓 ) 𝑟 ) 𝑠 𝑤 ) = ( ( 𝑞 𝑠 𝑤 ) 𝑎 ( 𝑟 𝑠 𝑤 ) ) ) ∧ ( ( ( 𝑞 ( .r ‘ 𝑓 ) 𝑟 ) 𝑠 𝑤 ) = ( 𝑞 𝑠 ( 𝑟 𝑠 𝑤 ) ) ∧ ( ( 1r ‘ 𝑓 ) 𝑠 𝑤 ) = 𝑤 ∧ ( ( 0g ‘ 𝑓 ) 𝑠 𝑤 ) = ( 0g ‘ 𝑔 ) ) ) ) ) |
32 |
18 31
|
raleqbidv |
⊢ ( ( 𝑘 = ( Base ‘ 𝑓 ) ∧ 𝑝 = ( +g ‘ 𝑓 ) ∧ 𝑡 = ( .r ‘ 𝑓 ) ) → ( ∀ 𝑞 ∈ 𝑘 ∀ 𝑟 ∈ 𝑘 ∀ 𝑥 ∈ 𝑣 ∀ 𝑤 ∈ 𝑣 ( ( ( 𝑟 𝑠 𝑤 ) ∈ 𝑣 ∧ ( 𝑟 𝑠 ( 𝑤 𝑎 𝑥 ) ) = ( ( 𝑟 𝑠 𝑤 ) 𝑎 ( 𝑟 𝑠 𝑥 ) ) ∧ ( ( 𝑞 𝑝 𝑟 ) 𝑠 𝑤 ) = ( ( 𝑞 𝑠 𝑤 ) 𝑎 ( 𝑟 𝑠 𝑤 ) ) ) ∧ ( ( ( 𝑞 𝑡 𝑟 ) 𝑠 𝑤 ) = ( 𝑞 𝑠 ( 𝑟 𝑠 𝑤 ) ) ∧ ( ( 1r ‘ 𝑓 ) 𝑠 𝑤 ) = 𝑤 ∧ ( ( 0g ‘ 𝑓 ) 𝑠 𝑤 ) = ( 0g ‘ 𝑔 ) ) ) ↔ ∀ 𝑞 ∈ ( Base ‘ 𝑓 ) ∀ 𝑟 ∈ ( Base ‘ 𝑓 ) ∀ 𝑥 ∈ 𝑣 ∀ 𝑤 ∈ 𝑣 ( ( ( 𝑟 𝑠 𝑤 ) ∈ 𝑣 ∧ ( 𝑟 𝑠 ( 𝑤 𝑎 𝑥 ) ) = ( ( 𝑟 𝑠 𝑤 ) 𝑎 ( 𝑟 𝑠 𝑥 ) ) ∧ ( ( 𝑞 ( +g ‘ 𝑓 ) 𝑟 ) 𝑠 𝑤 ) = ( ( 𝑞 𝑠 𝑤 ) 𝑎 ( 𝑟 𝑠 𝑤 ) ) ) ∧ ( ( ( 𝑞 ( .r ‘ 𝑓 ) 𝑟 ) 𝑠 𝑤 ) = ( 𝑞 𝑠 ( 𝑟 𝑠 𝑤 ) ) ∧ ( ( 1r ‘ 𝑓 ) 𝑠 𝑤 ) = 𝑤 ∧ ( ( 0g ‘ 𝑓 ) 𝑠 𝑤 ) = ( 0g ‘ 𝑔 ) ) ) ) ) |
33 |
32
|
anbi2d |
⊢ ( ( 𝑘 = ( Base ‘ 𝑓 ) ∧ 𝑝 = ( +g ‘ 𝑓 ) ∧ 𝑡 = ( .r ‘ 𝑓 ) ) → ( ( 𝑓 ∈ SRing ∧ ∀ 𝑞 ∈ 𝑘 ∀ 𝑟 ∈ 𝑘 ∀ 𝑥 ∈ 𝑣 ∀ 𝑤 ∈ 𝑣 ( ( ( 𝑟 𝑠 𝑤 ) ∈ 𝑣 ∧ ( 𝑟 𝑠 ( 𝑤 𝑎 𝑥 ) ) = ( ( 𝑟 𝑠 𝑤 ) 𝑎 ( 𝑟 𝑠 𝑥 ) ) ∧ ( ( 𝑞 𝑝 𝑟 ) 𝑠 𝑤 ) = ( ( 𝑞 𝑠 𝑤 ) 𝑎 ( 𝑟 𝑠 𝑤 ) ) ) ∧ ( ( ( 𝑞 𝑡 𝑟 ) 𝑠 𝑤 ) = ( 𝑞 𝑠 ( 𝑟 𝑠 𝑤 ) ) ∧ ( ( 1r ‘ 𝑓 ) 𝑠 𝑤 ) = 𝑤 ∧ ( ( 0g ‘ 𝑓 ) 𝑠 𝑤 ) = ( 0g ‘ 𝑔 ) ) ) ) ↔ ( 𝑓 ∈ SRing ∧ ∀ 𝑞 ∈ ( Base ‘ 𝑓 ) ∀ 𝑟 ∈ ( Base ‘ 𝑓 ) ∀ 𝑥 ∈ 𝑣 ∀ 𝑤 ∈ 𝑣 ( ( ( 𝑟 𝑠 𝑤 ) ∈ 𝑣 ∧ ( 𝑟 𝑠 ( 𝑤 𝑎 𝑥 ) ) = ( ( 𝑟 𝑠 𝑤 ) 𝑎 ( 𝑟 𝑠 𝑥 ) ) ∧ ( ( 𝑞 ( +g ‘ 𝑓 ) 𝑟 ) 𝑠 𝑤 ) = ( ( 𝑞 𝑠 𝑤 ) 𝑎 ( 𝑟 𝑠 𝑤 ) ) ) ∧ ( ( ( 𝑞 ( .r ‘ 𝑓 ) 𝑟 ) 𝑠 𝑤 ) = ( 𝑞 𝑠 ( 𝑟 𝑠 𝑤 ) ) ∧ ( ( 1r ‘ 𝑓 ) 𝑠 𝑤 ) = 𝑤 ∧ ( ( 0g ‘ 𝑓 ) 𝑠 𝑤 ) = ( 0g ‘ 𝑔 ) ) ) ) ) ) |
34 |
15 16 17 33
|
sbc3ie |
⊢ ( [ ( Base ‘ 𝑓 ) / 𝑘 ] [ ( +g ‘ 𝑓 ) / 𝑝 ] [ ( .r ‘ 𝑓 ) / 𝑡 ] ( 𝑓 ∈ SRing ∧ ∀ 𝑞 ∈ 𝑘 ∀ 𝑟 ∈ 𝑘 ∀ 𝑥 ∈ 𝑣 ∀ 𝑤 ∈ 𝑣 ( ( ( 𝑟 𝑠 𝑤 ) ∈ 𝑣 ∧ ( 𝑟 𝑠 ( 𝑤 𝑎 𝑥 ) ) = ( ( 𝑟 𝑠 𝑤 ) 𝑎 ( 𝑟 𝑠 𝑥 ) ) ∧ ( ( 𝑞 𝑝 𝑟 ) 𝑠 𝑤 ) = ( ( 𝑞 𝑠 𝑤 ) 𝑎 ( 𝑟 𝑠 𝑤 ) ) ) ∧ ( ( ( 𝑞 𝑡 𝑟 ) 𝑠 𝑤 ) = ( 𝑞 𝑠 ( 𝑟 𝑠 𝑤 ) ) ∧ ( ( 1r ‘ 𝑓 ) 𝑠 𝑤 ) = 𝑤 ∧ ( ( 0g ‘ 𝑓 ) 𝑠 𝑤 ) = ( 0g ‘ 𝑔 ) ) ) ) ↔ ( 𝑓 ∈ SRing ∧ ∀ 𝑞 ∈ ( Base ‘ 𝑓 ) ∀ 𝑟 ∈ ( Base ‘ 𝑓 ) ∀ 𝑥 ∈ 𝑣 ∀ 𝑤 ∈ 𝑣 ( ( ( 𝑟 𝑠 𝑤 ) ∈ 𝑣 ∧ ( 𝑟 𝑠 ( 𝑤 𝑎 𝑥 ) ) = ( ( 𝑟 𝑠 𝑤 ) 𝑎 ( 𝑟 𝑠 𝑥 ) ) ∧ ( ( 𝑞 ( +g ‘ 𝑓 ) 𝑟 ) 𝑠 𝑤 ) = ( ( 𝑞 𝑠 𝑤 ) 𝑎 ( 𝑟 𝑠 𝑤 ) ) ) ∧ ( ( ( 𝑞 ( .r ‘ 𝑓 ) 𝑟 ) 𝑠 𝑤 ) = ( 𝑞 𝑠 ( 𝑟 𝑠 𝑤 ) ) ∧ ( ( 1r ‘ 𝑓 ) 𝑠 𝑤 ) = 𝑤 ∧ ( ( 0g ‘ 𝑓 ) 𝑠 𝑤 ) = ( 0g ‘ 𝑔 ) ) ) ) ) |
35 |
|
simpr |
⊢ ( ( 𝑠 = ( ·𝑠 ‘ 𝑔 ) ∧ 𝑓 = ( Scalar ‘ 𝑔 ) ) → 𝑓 = ( Scalar ‘ 𝑔 ) ) |
36 |
35
|
eleq1d |
⊢ ( ( 𝑠 = ( ·𝑠 ‘ 𝑔 ) ∧ 𝑓 = ( Scalar ‘ 𝑔 ) ) → ( 𝑓 ∈ SRing ↔ ( Scalar ‘ 𝑔 ) ∈ SRing ) ) |
37 |
35
|
fveq2d |
⊢ ( ( 𝑠 = ( ·𝑠 ‘ 𝑔 ) ∧ 𝑓 = ( Scalar ‘ 𝑔 ) ) → ( Base ‘ 𝑓 ) = ( Base ‘ ( Scalar ‘ 𝑔 ) ) ) |
38 |
|
simpl |
⊢ ( ( 𝑠 = ( ·𝑠 ‘ 𝑔 ) ∧ 𝑓 = ( Scalar ‘ 𝑔 ) ) → 𝑠 = ( ·𝑠 ‘ 𝑔 ) ) |
39 |
38
|
oveqd |
⊢ ( ( 𝑠 = ( ·𝑠 ‘ 𝑔 ) ∧ 𝑓 = ( Scalar ‘ 𝑔 ) ) → ( 𝑟 𝑠 𝑤 ) = ( 𝑟 ( ·𝑠 ‘ 𝑔 ) 𝑤 ) ) |
40 |
39
|
eleq1d |
⊢ ( ( 𝑠 = ( ·𝑠 ‘ 𝑔 ) ∧ 𝑓 = ( Scalar ‘ 𝑔 ) ) → ( ( 𝑟 𝑠 𝑤 ) ∈ 𝑣 ↔ ( 𝑟 ( ·𝑠 ‘ 𝑔 ) 𝑤 ) ∈ 𝑣 ) ) |
41 |
38
|
oveqd |
⊢ ( ( 𝑠 = ( ·𝑠 ‘ 𝑔 ) ∧ 𝑓 = ( Scalar ‘ 𝑔 ) ) → ( 𝑟 𝑠 ( 𝑤 𝑎 𝑥 ) ) = ( 𝑟 ( ·𝑠 ‘ 𝑔 ) ( 𝑤 𝑎 𝑥 ) ) ) |
42 |
38
|
oveqd |
⊢ ( ( 𝑠 = ( ·𝑠 ‘ 𝑔 ) ∧ 𝑓 = ( Scalar ‘ 𝑔 ) ) → ( 𝑟 𝑠 𝑥 ) = ( 𝑟 ( ·𝑠 ‘ 𝑔 ) 𝑥 ) ) |
43 |
39 42
|
oveq12d |
⊢ ( ( 𝑠 = ( ·𝑠 ‘ 𝑔 ) ∧ 𝑓 = ( Scalar ‘ 𝑔 ) ) → ( ( 𝑟 𝑠 𝑤 ) 𝑎 ( 𝑟 𝑠 𝑥 ) ) = ( ( 𝑟 ( ·𝑠 ‘ 𝑔 ) 𝑤 ) 𝑎 ( 𝑟 ( ·𝑠 ‘ 𝑔 ) 𝑥 ) ) ) |
44 |
41 43
|
eqeq12d |
⊢ ( ( 𝑠 = ( ·𝑠 ‘ 𝑔 ) ∧ 𝑓 = ( Scalar ‘ 𝑔 ) ) → ( ( 𝑟 𝑠 ( 𝑤 𝑎 𝑥 ) ) = ( ( 𝑟 𝑠 𝑤 ) 𝑎 ( 𝑟 𝑠 𝑥 ) ) ↔ ( 𝑟 ( ·𝑠 ‘ 𝑔 ) ( 𝑤 𝑎 𝑥 ) ) = ( ( 𝑟 ( ·𝑠 ‘ 𝑔 ) 𝑤 ) 𝑎 ( 𝑟 ( ·𝑠 ‘ 𝑔 ) 𝑥 ) ) ) ) |
45 |
35
|
fveq2d |
⊢ ( ( 𝑠 = ( ·𝑠 ‘ 𝑔 ) ∧ 𝑓 = ( Scalar ‘ 𝑔 ) ) → ( +g ‘ 𝑓 ) = ( +g ‘ ( Scalar ‘ 𝑔 ) ) ) |
46 |
45
|
oveqd |
⊢ ( ( 𝑠 = ( ·𝑠 ‘ 𝑔 ) ∧ 𝑓 = ( Scalar ‘ 𝑔 ) ) → ( 𝑞 ( +g ‘ 𝑓 ) 𝑟 ) = ( 𝑞 ( +g ‘ ( Scalar ‘ 𝑔 ) ) 𝑟 ) ) |
47 |
|
eqidd |
⊢ ( ( 𝑠 = ( ·𝑠 ‘ 𝑔 ) ∧ 𝑓 = ( Scalar ‘ 𝑔 ) ) → 𝑤 = 𝑤 ) |
48 |
38 46 47
|
oveq123d |
⊢ ( ( 𝑠 = ( ·𝑠 ‘ 𝑔 ) ∧ 𝑓 = ( Scalar ‘ 𝑔 ) ) → ( ( 𝑞 ( +g ‘ 𝑓 ) 𝑟 ) 𝑠 𝑤 ) = ( ( 𝑞 ( +g ‘ ( Scalar ‘ 𝑔 ) ) 𝑟 ) ( ·𝑠 ‘ 𝑔 ) 𝑤 ) ) |
49 |
38
|
oveqd |
⊢ ( ( 𝑠 = ( ·𝑠 ‘ 𝑔 ) ∧ 𝑓 = ( Scalar ‘ 𝑔 ) ) → ( 𝑞 𝑠 𝑤 ) = ( 𝑞 ( ·𝑠 ‘ 𝑔 ) 𝑤 ) ) |
50 |
49 39
|
oveq12d |
⊢ ( ( 𝑠 = ( ·𝑠 ‘ 𝑔 ) ∧ 𝑓 = ( Scalar ‘ 𝑔 ) ) → ( ( 𝑞 𝑠 𝑤 ) 𝑎 ( 𝑟 𝑠 𝑤 ) ) = ( ( 𝑞 ( ·𝑠 ‘ 𝑔 ) 𝑤 ) 𝑎 ( 𝑟 ( ·𝑠 ‘ 𝑔 ) 𝑤 ) ) ) |
51 |
48 50
|
eqeq12d |
⊢ ( ( 𝑠 = ( ·𝑠 ‘ 𝑔 ) ∧ 𝑓 = ( Scalar ‘ 𝑔 ) ) → ( ( ( 𝑞 ( +g ‘ 𝑓 ) 𝑟 ) 𝑠 𝑤 ) = ( ( 𝑞 𝑠 𝑤 ) 𝑎 ( 𝑟 𝑠 𝑤 ) ) ↔ ( ( 𝑞 ( +g ‘ ( Scalar ‘ 𝑔 ) ) 𝑟 ) ( ·𝑠 ‘ 𝑔 ) 𝑤 ) = ( ( 𝑞 ( ·𝑠 ‘ 𝑔 ) 𝑤 ) 𝑎 ( 𝑟 ( ·𝑠 ‘ 𝑔 ) 𝑤 ) ) ) ) |
52 |
40 44 51
|
3anbi123d |
⊢ ( ( 𝑠 = ( ·𝑠 ‘ 𝑔 ) ∧ 𝑓 = ( Scalar ‘ 𝑔 ) ) → ( ( ( 𝑟 𝑠 𝑤 ) ∈ 𝑣 ∧ ( 𝑟 𝑠 ( 𝑤 𝑎 𝑥 ) ) = ( ( 𝑟 𝑠 𝑤 ) 𝑎 ( 𝑟 𝑠 𝑥 ) ) ∧ ( ( 𝑞 ( +g ‘ 𝑓 ) 𝑟 ) 𝑠 𝑤 ) = ( ( 𝑞 𝑠 𝑤 ) 𝑎 ( 𝑟 𝑠 𝑤 ) ) ) ↔ ( ( 𝑟 ( ·𝑠 ‘ 𝑔 ) 𝑤 ) ∈ 𝑣 ∧ ( 𝑟 ( ·𝑠 ‘ 𝑔 ) ( 𝑤 𝑎 𝑥 ) ) = ( ( 𝑟 ( ·𝑠 ‘ 𝑔 ) 𝑤 ) 𝑎 ( 𝑟 ( ·𝑠 ‘ 𝑔 ) 𝑥 ) ) ∧ ( ( 𝑞 ( +g ‘ ( Scalar ‘ 𝑔 ) ) 𝑟 ) ( ·𝑠 ‘ 𝑔 ) 𝑤 ) = ( ( 𝑞 ( ·𝑠 ‘ 𝑔 ) 𝑤 ) 𝑎 ( 𝑟 ( ·𝑠 ‘ 𝑔 ) 𝑤 ) ) ) ) ) |
53 |
35
|
fveq2d |
⊢ ( ( 𝑠 = ( ·𝑠 ‘ 𝑔 ) ∧ 𝑓 = ( Scalar ‘ 𝑔 ) ) → ( .r ‘ 𝑓 ) = ( .r ‘ ( Scalar ‘ 𝑔 ) ) ) |
54 |
53
|
oveqd |
⊢ ( ( 𝑠 = ( ·𝑠 ‘ 𝑔 ) ∧ 𝑓 = ( Scalar ‘ 𝑔 ) ) → ( 𝑞 ( .r ‘ 𝑓 ) 𝑟 ) = ( 𝑞 ( .r ‘ ( Scalar ‘ 𝑔 ) ) 𝑟 ) ) |
55 |
38 54 47
|
oveq123d |
⊢ ( ( 𝑠 = ( ·𝑠 ‘ 𝑔 ) ∧ 𝑓 = ( Scalar ‘ 𝑔 ) ) → ( ( 𝑞 ( .r ‘ 𝑓 ) 𝑟 ) 𝑠 𝑤 ) = ( ( 𝑞 ( .r ‘ ( Scalar ‘ 𝑔 ) ) 𝑟 ) ( ·𝑠 ‘ 𝑔 ) 𝑤 ) ) |
56 |
|
eqidd |
⊢ ( ( 𝑠 = ( ·𝑠 ‘ 𝑔 ) ∧ 𝑓 = ( Scalar ‘ 𝑔 ) ) → 𝑞 = 𝑞 ) |
57 |
38 56 39
|
oveq123d |
⊢ ( ( 𝑠 = ( ·𝑠 ‘ 𝑔 ) ∧ 𝑓 = ( Scalar ‘ 𝑔 ) ) → ( 𝑞 𝑠 ( 𝑟 𝑠 𝑤 ) ) = ( 𝑞 ( ·𝑠 ‘ 𝑔 ) ( 𝑟 ( ·𝑠 ‘ 𝑔 ) 𝑤 ) ) ) |
58 |
55 57
|
eqeq12d |
⊢ ( ( 𝑠 = ( ·𝑠 ‘ 𝑔 ) ∧ 𝑓 = ( Scalar ‘ 𝑔 ) ) → ( ( ( 𝑞 ( .r ‘ 𝑓 ) 𝑟 ) 𝑠 𝑤 ) = ( 𝑞 𝑠 ( 𝑟 𝑠 𝑤 ) ) ↔ ( ( 𝑞 ( .r ‘ ( Scalar ‘ 𝑔 ) ) 𝑟 ) ( ·𝑠 ‘ 𝑔 ) 𝑤 ) = ( 𝑞 ( ·𝑠 ‘ 𝑔 ) ( 𝑟 ( ·𝑠 ‘ 𝑔 ) 𝑤 ) ) ) ) |
59 |
35
|
fveq2d |
⊢ ( ( 𝑠 = ( ·𝑠 ‘ 𝑔 ) ∧ 𝑓 = ( Scalar ‘ 𝑔 ) ) → ( 1r ‘ 𝑓 ) = ( 1r ‘ ( Scalar ‘ 𝑔 ) ) ) |
60 |
38 59 47
|
oveq123d |
⊢ ( ( 𝑠 = ( ·𝑠 ‘ 𝑔 ) ∧ 𝑓 = ( Scalar ‘ 𝑔 ) ) → ( ( 1r ‘ 𝑓 ) 𝑠 𝑤 ) = ( ( 1r ‘ ( Scalar ‘ 𝑔 ) ) ( ·𝑠 ‘ 𝑔 ) 𝑤 ) ) |
61 |
60
|
eqeq1d |
⊢ ( ( 𝑠 = ( ·𝑠 ‘ 𝑔 ) ∧ 𝑓 = ( Scalar ‘ 𝑔 ) ) → ( ( ( 1r ‘ 𝑓 ) 𝑠 𝑤 ) = 𝑤 ↔ ( ( 1r ‘ ( Scalar ‘ 𝑔 ) ) ( ·𝑠 ‘ 𝑔 ) 𝑤 ) = 𝑤 ) ) |
62 |
35
|
fveq2d |
⊢ ( ( 𝑠 = ( ·𝑠 ‘ 𝑔 ) ∧ 𝑓 = ( Scalar ‘ 𝑔 ) ) → ( 0g ‘ 𝑓 ) = ( 0g ‘ ( Scalar ‘ 𝑔 ) ) ) |
63 |
38 62 47
|
oveq123d |
⊢ ( ( 𝑠 = ( ·𝑠 ‘ 𝑔 ) ∧ 𝑓 = ( Scalar ‘ 𝑔 ) ) → ( ( 0g ‘ 𝑓 ) 𝑠 𝑤 ) = ( ( 0g ‘ ( Scalar ‘ 𝑔 ) ) ( ·𝑠 ‘ 𝑔 ) 𝑤 ) ) |
64 |
63
|
eqeq1d |
⊢ ( ( 𝑠 = ( ·𝑠 ‘ 𝑔 ) ∧ 𝑓 = ( Scalar ‘ 𝑔 ) ) → ( ( ( 0g ‘ 𝑓 ) 𝑠 𝑤 ) = ( 0g ‘ 𝑔 ) ↔ ( ( 0g ‘ ( Scalar ‘ 𝑔 ) ) ( ·𝑠 ‘ 𝑔 ) 𝑤 ) = ( 0g ‘ 𝑔 ) ) ) |
65 |
58 61 64
|
3anbi123d |
⊢ ( ( 𝑠 = ( ·𝑠 ‘ 𝑔 ) ∧ 𝑓 = ( Scalar ‘ 𝑔 ) ) → ( ( ( ( 𝑞 ( .r ‘ 𝑓 ) 𝑟 ) 𝑠 𝑤 ) = ( 𝑞 𝑠 ( 𝑟 𝑠 𝑤 ) ) ∧ ( ( 1r ‘ 𝑓 ) 𝑠 𝑤 ) = 𝑤 ∧ ( ( 0g ‘ 𝑓 ) 𝑠 𝑤 ) = ( 0g ‘ 𝑔 ) ) ↔ ( ( ( 𝑞 ( .r ‘ ( Scalar ‘ 𝑔 ) ) 𝑟 ) ( ·𝑠 ‘ 𝑔 ) 𝑤 ) = ( 𝑞 ( ·𝑠 ‘ 𝑔 ) ( 𝑟 ( ·𝑠 ‘ 𝑔 ) 𝑤 ) ) ∧ ( ( 1r ‘ ( Scalar ‘ 𝑔 ) ) ( ·𝑠 ‘ 𝑔 ) 𝑤 ) = 𝑤 ∧ ( ( 0g ‘ ( Scalar ‘ 𝑔 ) ) ( ·𝑠 ‘ 𝑔 ) 𝑤 ) = ( 0g ‘ 𝑔 ) ) ) ) |
66 |
52 65
|
anbi12d |
⊢ ( ( 𝑠 = ( ·𝑠 ‘ 𝑔 ) ∧ 𝑓 = ( Scalar ‘ 𝑔 ) ) → ( ( ( ( 𝑟 𝑠 𝑤 ) ∈ 𝑣 ∧ ( 𝑟 𝑠 ( 𝑤 𝑎 𝑥 ) ) = ( ( 𝑟 𝑠 𝑤 ) 𝑎 ( 𝑟 𝑠 𝑥 ) ) ∧ ( ( 𝑞 ( +g ‘ 𝑓 ) 𝑟 ) 𝑠 𝑤 ) = ( ( 𝑞 𝑠 𝑤 ) 𝑎 ( 𝑟 𝑠 𝑤 ) ) ) ∧ ( ( ( 𝑞 ( .r ‘ 𝑓 ) 𝑟 ) 𝑠 𝑤 ) = ( 𝑞 𝑠 ( 𝑟 𝑠 𝑤 ) ) ∧ ( ( 1r ‘ 𝑓 ) 𝑠 𝑤 ) = 𝑤 ∧ ( ( 0g ‘ 𝑓 ) 𝑠 𝑤 ) = ( 0g ‘ 𝑔 ) ) ) ↔ ( ( ( 𝑟 ( ·𝑠 ‘ 𝑔 ) 𝑤 ) ∈ 𝑣 ∧ ( 𝑟 ( ·𝑠 ‘ 𝑔 ) ( 𝑤 𝑎 𝑥 ) ) = ( ( 𝑟 ( ·𝑠 ‘ 𝑔 ) 𝑤 ) 𝑎 ( 𝑟 ( ·𝑠 ‘ 𝑔 ) 𝑥 ) ) ∧ ( ( 𝑞 ( +g ‘ ( Scalar ‘ 𝑔 ) ) 𝑟 ) ( ·𝑠 ‘ 𝑔 ) 𝑤 ) = ( ( 𝑞 ( ·𝑠 ‘ 𝑔 ) 𝑤 ) 𝑎 ( 𝑟 ( ·𝑠 ‘ 𝑔 ) 𝑤 ) ) ) ∧ ( ( ( 𝑞 ( .r ‘ ( Scalar ‘ 𝑔 ) ) 𝑟 ) ( ·𝑠 ‘ 𝑔 ) 𝑤 ) = ( 𝑞 ( ·𝑠 ‘ 𝑔 ) ( 𝑟 ( ·𝑠 ‘ 𝑔 ) 𝑤 ) ) ∧ ( ( 1r ‘ ( Scalar ‘ 𝑔 ) ) ( ·𝑠 ‘ 𝑔 ) 𝑤 ) = 𝑤 ∧ ( ( 0g ‘ ( Scalar ‘ 𝑔 ) ) ( ·𝑠 ‘ 𝑔 ) 𝑤 ) = ( 0g ‘ 𝑔 ) ) ) ) ) |
67 |
66
|
2ralbidv |
⊢ ( ( 𝑠 = ( ·𝑠 ‘ 𝑔 ) ∧ 𝑓 = ( Scalar ‘ 𝑔 ) ) → ( ∀ 𝑥 ∈ 𝑣 ∀ 𝑤 ∈ 𝑣 ( ( ( 𝑟 𝑠 𝑤 ) ∈ 𝑣 ∧ ( 𝑟 𝑠 ( 𝑤 𝑎 𝑥 ) ) = ( ( 𝑟 𝑠 𝑤 ) 𝑎 ( 𝑟 𝑠 𝑥 ) ) ∧ ( ( 𝑞 ( +g ‘ 𝑓 ) 𝑟 ) 𝑠 𝑤 ) = ( ( 𝑞 𝑠 𝑤 ) 𝑎 ( 𝑟 𝑠 𝑤 ) ) ) ∧ ( ( ( 𝑞 ( .r ‘ 𝑓 ) 𝑟 ) 𝑠 𝑤 ) = ( 𝑞 𝑠 ( 𝑟 𝑠 𝑤 ) ) ∧ ( ( 1r ‘ 𝑓 ) 𝑠 𝑤 ) = 𝑤 ∧ ( ( 0g ‘ 𝑓 ) 𝑠 𝑤 ) = ( 0g ‘ 𝑔 ) ) ) ↔ ∀ 𝑥 ∈ 𝑣 ∀ 𝑤 ∈ 𝑣 ( ( ( 𝑟 ( ·𝑠 ‘ 𝑔 ) 𝑤 ) ∈ 𝑣 ∧ ( 𝑟 ( ·𝑠 ‘ 𝑔 ) ( 𝑤 𝑎 𝑥 ) ) = ( ( 𝑟 ( ·𝑠 ‘ 𝑔 ) 𝑤 ) 𝑎 ( 𝑟 ( ·𝑠 ‘ 𝑔 ) 𝑥 ) ) ∧ ( ( 𝑞 ( +g ‘ ( Scalar ‘ 𝑔 ) ) 𝑟 ) ( ·𝑠 ‘ 𝑔 ) 𝑤 ) = ( ( 𝑞 ( ·𝑠 ‘ 𝑔 ) 𝑤 ) 𝑎 ( 𝑟 ( ·𝑠 ‘ 𝑔 ) 𝑤 ) ) ) ∧ ( ( ( 𝑞 ( .r ‘ ( Scalar ‘ 𝑔 ) ) 𝑟 ) ( ·𝑠 ‘ 𝑔 ) 𝑤 ) = ( 𝑞 ( ·𝑠 ‘ 𝑔 ) ( 𝑟 ( ·𝑠 ‘ 𝑔 ) 𝑤 ) ) ∧ ( ( 1r ‘ ( Scalar ‘ 𝑔 ) ) ( ·𝑠 ‘ 𝑔 ) 𝑤 ) = 𝑤 ∧ ( ( 0g ‘ ( Scalar ‘ 𝑔 ) ) ( ·𝑠 ‘ 𝑔 ) 𝑤 ) = ( 0g ‘ 𝑔 ) ) ) ) ) |
68 |
37 67
|
raleqbidv |
⊢ ( ( 𝑠 = ( ·𝑠 ‘ 𝑔 ) ∧ 𝑓 = ( Scalar ‘ 𝑔 ) ) → ( ∀ 𝑟 ∈ ( Base ‘ 𝑓 ) ∀ 𝑥 ∈ 𝑣 ∀ 𝑤 ∈ 𝑣 ( ( ( 𝑟 𝑠 𝑤 ) ∈ 𝑣 ∧ ( 𝑟 𝑠 ( 𝑤 𝑎 𝑥 ) ) = ( ( 𝑟 𝑠 𝑤 ) 𝑎 ( 𝑟 𝑠 𝑥 ) ) ∧ ( ( 𝑞 ( +g ‘ 𝑓 ) 𝑟 ) 𝑠 𝑤 ) = ( ( 𝑞 𝑠 𝑤 ) 𝑎 ( 𝑟 𝑠 𝑤 ) ) ) ∧ ( ( ( 𝑞 ( .r ‘ 𝑓 ) 𝑟 ) 𝑠 𝑤 ) = ( 𝑞 𝑠 ( 𝑟 𝑠 𝑤 ) ) ∧ ( ( 1r ‘ 𝑓 ) 𝑠 𝑤 ) = 𝑤 ∧ ( ( 0g ‘ 𝑓 ) 𝑠 𝑤 ) = ( 0g ‘ 𝑔 ) ) ) ↔ ∀ 𝑟 ∈ ( Base ‘ ( Scalar ‘ 𝑔 ) ) ∀ 𝑥 ∈ 𝑣 ∀ 𝑤 ∈ 𝑣 ( ( ( 𝑟 ( ·𝑠 ‘ 𝑔 ) 𝑤 ) ∈ 𝑣 ∧ ( 𝑟 ( ·𝑠 ‘ 𝑔 ) ( 𝑤 𝑎 𝑥 ) ) = ( ( 𝑟 ( ·𝑠 ‘ 𝑔 ) 𝑤 ) 𝑎 ( 𝑟 ( ·𝑠 ‘ 𝑔 ) 𝑥 ) ) ∧ ( ( 𝑞 ( +g ‘ ( Scalar ‘ 𝑔 ) ) 𝑟 ) ( ·𝑠 ‘ 𝑔 ) 𝑤 ) = ( ( 𝑞 ( ·𝑠 ‘ 𝑔 ) 𝑤 ) 𝑎 ( 𝑟 ( ·𝑠 ‘ 𝑔 ) 𝑤 ) ) ) ∧ ( ( ( 𝑞 ( .r ‘ ( Scalar ‘ 𝑔 ) ) 𝑟 ) ( ·𝑠 ‘ 𝑔 ) 𝑤 ) = ( 𝑞 ( ·𝑠 ‘ 𝑔 ) ( 𝑟 ( ·𝑠 ‘ 𝑔 ) 𝑤 ) ) ∧ ( ( 1r ‘ ( Scalar ‘ 𝑔 ) ) ( ·𝑠 ‘ 𝑔 ) 𝑤 ) = 𝑤 ∧ ( ( 0g ‘ ( Scalar ‘ 𝑔 ) ) ( ·𝑠 ‘ 𝑔 ) 𝑤 ) = ( 0g ‘ 𝑔 ) ) ) ) ) |
69 |
37 68
|
raleqbidv |
⊢ ( ( 𝑠 = ( ·𝑠 ‘ 𝑔 ) ∧ 𝑓 = ( Scalar ‘ 𝑔 ) ) → ( ∀ 𝑞 ∈ ( Base ‘ 𝑓 ) ∀ 𝑟 ∈ ( Base ‘ 𝑓 ) ∀ 𝑥 ∈ 𝑣 ∀ 𝑤 ∈ 𝑣 ( ( ( 𝑟 𝑠 𝑤 ) ∈ 𝑣 ∧ ( 𝑟 𝑠 ( 𝑤 𝑎 𝑥 ) ) = ( ( 𝑟 𝑠 𝑤 ) 𝑎 ( 𝑟 𝑠 𝑥 ) ) ∧ ( ( 𝑞 ( +g ‘ 𝑓 ) 𝑟 ) 𝑠 𝑤 ) = ( ( 𝑞 𝑠 𝑤 ) 𝑎 ( 𝑟 𝑠 𝑤 ) ) ) ∧ ( ( ( 𝑞 ( .r ‘ 𝑓 ) 𝑟 ) 𝑠 𝑤 ) = ( 𝑞 𝑠 ( 𝑟 𝑠 𝑤 ) ) ∧ ( ( 1r ‘ 𝑓 ) 𝑠 𝑤 ) = 𝑤 ∧ ( ( 0g ‘ 𝑓 ) 𝑠 𝑤 ) = ( 0g ‘ 𝑔 ) ) ) ↔ ∀ 𝑞 ∈ ( Base ‘ ( Scalar ‘ 𝑔 ) ) ∀ 𝑟 ∈ ( Base ‘ ( Scalar ‘ 𝑔 ) ) ∀ 𝑥 ∈ 𝑣 ∀ 𝑤 ∈ 𝑣 ( ( ( 𝑟 ( ·𝑠 ‘ 𝑔 ) 𝑤 ) ∈ 𝑣 ∧ ( 𝑟 ( ·𝑠 ‘ 𝑔 ) ( 𝑤 𝑎 𝑥 ) ) = ( ( 𝑟 ( ·𝑠 ‘ 𝑔 ) 𝑤 ) 𝑎 ( 𝑟 ( ·𝑠 ‘ 𝑔 ) 𝑥 ) ) ∧ ( ( 𝑞 ( +g ‘ ( Scalar ‘ 𝑔 ) ) 𝑟 ) ( ·𝑠 ‘ 𝑔 ) 𝑤 ) = ( ( 𝑞 ( ·𝑠 ‘ 𝑔 ) 𝑤 ) 𝑎 ( 𝑟 ( ·𝑠 ‘ 𝑔 ) 𝑤 ) ) ) ∧ ( ( ( 𝑞 ( .r ‘ ( Scalar ‘ 𝑔 ) ) 𝑟 ) ( ·𝑠 ‘ 𝑔 ) 𝑤 ) = ( 𝑞 ( ·𝑠 ‘ 𝑔 ) ( 𝑟 ( ·𝑠 ‘ 𝑔 ) 𝑤 ) ) ∧ ( ( 1r ‘ ( Scalar ‘ 𝑔 ) ) ( ·𝑠 ‘ 𝑔 ) 𝑤 ) = 𝑤 ∧ ( ( 0g ‘ ( Scalar ‘ 𝑔 ) ) ( ·𝑠 ‘ 𝑔 ) 𝑤 ) = ( 0g ‘ 𝑔 ) ) ) ) ) |
70 |
36 69
|
anbi12d |
⊢ ( ( 𝑠 = ( ·𝑠 ‘ 𝑔 ) ∧ 𝑓 = ( Scalar ‘ 𝑔 ) ) → ( ( 𝑓 ∈ SRing ∧ ∀ 𝑞 ∈ ( Base ‘ 𝑓 ) ∀ 𝑟 ∈ ( Base ‘ 𝑓 ) ∀ 𝑥 ∈ 𝑣 ∀ 𝑤 ∈ 𝑣 ( ( ( 𝑟 𝑠 𝑤 ) ∈ 𝑣 ∧ ( 𝑟 𝑠 ( 𝑤 𝑎 𝑥 ) ) = ( ( 𝑟 𝑠 𝑤 ) 𝑎 ( 𝑟 𝑠 𝑥 ) ) ∧ ( ( 𝑞 ( +g ‘ 𝑓 ) 𝑟 ) 𝑠 𝑤 ) = ( ( 𝑞 𝑠 𝑤 ) 𝑎 ( 𝑟 𝑠 𝑤 ) ) ) ∧ ( ( ( 𝑞 ( .r ‘ 𝑓 ) 𝑟 ) 𝑠 𝑤 ) = ( 𝑞 𝑠 ( 𝑟 𝑠 𝑤 ) ) ∧ ( ( 1r ‘ 𝑓 ) 𝑠 𝑤 ) = 𝑤 ∧ ( ( 0g ‘ 𝑓 ) 𝑠 𝑤 ) = ( 0g ‘ 𝑔 ) ) ) ) ↔ ( ( Scalar ‘ 𝑔 ) ∈ SRing ∧ ∀ 𝑞 ∈ ( Base ‘ ( Scalar ‘ 𝑔 ) ) ∀ 𝑟 ∈ ( Base ‘ ( Scalar ‘ 𝑔 ) ) ∀ 𝑥 ∈ 𝑣 ∀ 𝑤 ∈ 𝑣 ( ( ( 𝑟 ( ·𝑠 ‘ 𝑔 ) 𝑤 ) ∈ 𝑣 ∧ ( 𝑟 ( ·𝑠 ‘ 𝑔 ) ( 𝑤 𝑎 𝑥 ) ) = ( ( 𝑟 ( ·𝑠 ‘ 𝑔 ) 𝑤 ) 𝑎 ( 𝑟 ( ·𝑠 ‘ 𝑔 ) 𝑥 ) ) ∧ ( ( 𝑞 ( +g ‘ ( Scalar ‘ 𝑔 ) ) 𝑟 ) ( ·𝑠 ‘ 𝑔 ) 𝑤 ) = ( ( 𝑞 ( ·𝑠 ‘ 𝑔 ) 𝑤 ) 𝑎 ( 𝑟 ( ·𝑠 ‘ 𝑔 ) 𝑤 ) ) ) ∧ ( ( ( 𝑞 ( .r ‘ ( Scalar ‘ 𝑔 ) ) 𝑟 ) ( ·𝑠 ‘ 𝑔 ) 𝑤 ) = ( 𝑞 ( ·𝑠 ‘ 𝑔 ) ( 𝑟 ( ·𝑠 ‘ 𝑔 ) 𝑤 ) ) ∧ ( ( 1r ‘ ( Scalar ‘ 𝑔 ) ) ( ·𝑠 ‘ 𝑔 ) 𝑤 ) = 𝑤 ∧ ( ( 0g ‘ ( Scalar ‘ 𝑔 ) ) ( ·𝑠 ‘ 𝑔 ) 𝑤 ) = ( 0g ‘ 𝑔 ) ) ) ) ) ) |
71 |
34 70
|
syl5bb |
⊢ ( ( 𝑠 = ( ·𝑠 ‘ 𝑔 ) ∧ 𝑓 = ( Scalar ‘ 𝑔 ) ) → ( [ ( Base ‘ 𝑓 ) / 𝑘 ] [ ( +g ‘ 𝑓 ) / 𝑝 ] [ ( .r ‘ 𝑓 ) / 𝑡 ] ( 𝑓 ∈ SRing ∧ ∀ 𝑞 ∈ 𝑘 ∀ 𝑟 ∈ 𝑘 ∀ 𝑥 ∈ 𝑣 ∀ 𝑤 ∈ 𝑣 ( ( ( 𝑟 𝑠 𝑤 ) ∈ 𝑣 ∧ ( 𝑟 𝑠 ( 𝑤 𝑎 𝑥 ) ) = ( ( 𝑟 𝑠 𝑤 ) 𝑎 ( 𝑟 𝑠 𝑥 ) ) ∧ ( ( 𝑞 𝑝 𝑟 ) 𝑠 𝑤 ) = ( ( 𝑞 𝑠 𝑤 ) 𝑎 ( 𝑟 𝑠 𝑤 ) ) ) ∧ ( ( ( 𝑞 𝑡 𝑟 ) 𝑠 𝑤 ) = ( 𝑞 𝑠 ( 𝑟 𝑠 𝑤 ) ) ∧ ( ( 1r ‘ 𝑓 ) 𝑠 𝑤 ) = 𝑤 ∧ ( ( 0g ‘ 𝑓 ) 𝑠 𝑤 ) = ( 0g ‘ 𝑔 ) ) ) ) ↔ ( ( Scalar ‘ 𝑔 ) ∈ SRing ∧ ∀ 𝑞 ∈ ( Base ‘ ( Scalar ‘ 𝑔 ) ) ∀ 𝑟 ∈ ( Base ‘ ( Scalar ‘ 𝑔 ) ) ∀ 𝑥 ∈ 𝑣 ∀ 𝑤 ∈ 𝑣 ( ( ( 𝑟 ( ·𝑠 ‘ 𝑔 ) 𝑤 ) ∈ 𝑣 ∧ ( 𝑟 ( ·𝑠 ‘ 𝑔 ) ( 𝑤 𝑎 𝑥 ) ) = ( ( 𝑟 ( ·𝑠 ‘ 𝑔 ) 𝑤 ) 𝑎 ( 𝑟 ( ·𝑠 ‘ 𝑔 ) 𝑥 ) ) ∧ ( ( 𝑞 ( +g ‘ ( Scalar ‘ 𝑔 ) ) 𝑟 ) ( ·𝑠 ‘ 𝑔 ) 𝑤 ) = ( ( 𝑞 ( ·𝑠 ‘ 𝑔 ) 𝑤 ) 𝑎 ( 𝑟 ( ·𝑠 ‘ 𝑔 ) 𝑤 ) ) ) ∧ ( ( ( 𝑞 ( .r ‘ ( Scalar ‘ 𝑔 ) ) 𝑟 ) ( ·𝑠 ‘ 𝑔 ) 𝑤 ) = ( 𝑞 ( ·𝑠 ‘ 𝑔 ) ( 𝑟 ( ·𝑠 ‘ 𝑔 ) 𝑤 ) ) ∧ ( ( 1r ‘ ( Scalar ‘ 𝑔 ) ) ( ·𝑠 ‘ 𝑔 ) 𝑤 ) = 𝑤 ∧ ( ( 0g ‘ ( Scalar ‘ 𝑔 ) ) ( ·𝑠 ‘ 𝑔 ) 𝑤 ) = ( 0g ‘ 𝑔 ) ) ) ) ) ) |
72 |
13 14 71
|
sbc2ie |
⊢ ( [ ( ·𝑠 ‘ 𝑔 ) / 𝑠 ] [ ( Scalar ‘ 𝑔 ) / 𝑓 ] [ ( Base ‘ 𝑓 ) / 𝑘 ] [ ( +g ‘ 𝑓 ) / 𝑝 ] [ ( .r ‘ 𝑓 ) / 𝑡 ] ( 𝑓 ∈ SRing ∧ ∀ 𝑞 ∈ 𝑘 ∀ 𝑟 ∈ 𝑘 ∀ 𝑥 ∈ 𝑣 ∀ 𝑤 ∈ 𝑣 ( ( ( 𝑟 𝑠 𝑤 ) ∈ 𝑣 ∧ ( 𝑟 𝑠 ( 𝑤 𝑎 𝑥 ) ) = ( ( 𝑟 𝑠 𝑤 ) 𝑎 ( 𝑟 𝑠 𝑥 ) ) ∧ ( ( 𝑞 𝑝 𝑟 ) 𝑠 𝑤 ) = ( ( 𝑞 𝑠 𝑤 ) 𝑎 ( 𝑟 𝑠 𝑤 ) ) ) ∧ ( ( ( 𝑞 𝑡 𝑟 ) 𝑠 𝑤 ) = ( 𝑞 𝑠 ( 𝑟 𝑠 𝑤 ) ) ∧ ( ( 1r ‘ 𝑓 ) 𝑠 𝑤 ) = 𝑤 ∧ ( ( 0g ‘ 𝑓 ) 𝑠 𝑤 ) = ( 0g ‘ 𝑔 ) ) ) ) ↔ ( ( Scalar ‘ 𝑔 ) ∈ SRing ∧ ∀ 𝑞 ∈ ( Base ‘ ( Scalar ‘ 𝑔 ) ) ∀ 𝑟 ∈ ( Base ‘ ( Scalar ‘ 𝑔 ) ) ∀ 𝑥 ∈ 𝑣 ∀ 𝑤 ∈ 𝑣 ( ( ( 𝑟 ( ·𝑠 ‘ 𝑔 ) 𝑤 ) ∈ 𝑣 ∧ ( 𝑟 ( ·𝑠 ‘ 𝑔 ) ( 𝑤 𝑎 𝑥 ) ) = ( ( 𝑟 ( ·𝑠 ‘ 𝑔 ) 𝑤 ) 𝑎 ( 𝑟 ( ·𝑠 ‘ 𝑔 ) 𝑥 ) ) ∧ ( ( 𝑞 ( +g ‘ ( Scalar ‘ 𝑔 ) ) 𝑟 ) ( ·𝑠 ‘ 𝑔 ) 𝑤 ) = ( ( 𝑞 ( ·𝑠 ‘ 𝑔 ) 𝑤 ) 𝑎 ( 𝑟 ( ·𝑠 ‘ 𝑔 ) 𝑤 ) ) ) ∧ ( ( ( 𝑞 ( .r ‘ ( Scalar ‘ 𝑔 ) ) 𝑟 ) ( ·𝑠 ‘ 𝑔 ) 𝑤 ) = ( 𝑞 ( ·𝑠 ‘ 𝑔 ) ( 𝑟 ( ·𝑠 ‘ 𝑔 ) 𝑤 ) ) ∧ ( ( 1r ‘ ( Scalar ‘ 𝑔 ) ) ( ·𝑠 ‘ 𝑔 ) 𝑤 ) = 𝑤 ∧ ( ( 0g ‘ ( Scalar ‘ 𝑔 ) ) ( ·𝑠 ‘ 𝑔 ) 𝑤 ) = ( 0g ‘ 𝑔 ) ) ) ) ) |
73 |
|
simpl |
⊢ ( ( 𝑣 = ( Base ‘ 𝑔 ) ∧ 𝑎 = ( +g ‘ 𝑔 ) ) → 𝑣 = ( Base ‘ 𝑔 ) ) |
74 |
73
|
eleq2d |
⊢ ( ( 𝑣 = ( Base ‘ 𝑔 ) ∧ 𝑎 = ( +g ‘ 𝑔 ) ) → ( ( 𝑟 ( ·𝑠 ‘ 𝑔 ) 𝑤 ) ∈ 𝑣 ↔ ( 𝑟 ( ·𝑠 ‘ 𝑔 ) 𝑤 ) ∈ ( Base ‘ 𝑔 ) ) ) |
75 |
|
simpr |
⊢ ( ( 𝑣 = ( Base ‘ 𝑔 ) ∧ 𝑎 = ( +g ‘ 𝑔 ) ) → 𝑎 = ( +g ‘ 𝑔 ) ) |
76 |
75
|
oveqd |
⊢ ( ( 𝑣 = ( Base ‘ 𝑔 ) ∧ 𝑎 = ( +g ‘ 𝑔 ) ) → ( 𝑤 𝑎 𝑥 ) = ( 𝑤 ( +g ‘ 𝑔 ) 𝑥 ) ) |
77 |
76
|
oveq2d |
⊢ ( ( 𝑣 = ( Base ‘ 𝑔 ) ∧ 𝑎 = ( +g ‘ 𝑔 ) ) → ( 𝑟 ( ·𝑠 ‘ 𝑔 ) ( 𝑤 𝑎 𝑥 ) ) = ( 𝑟 ( ·𝑠 ‘ 𝑔 ) ( 𝑤 ( +g ‘ 𝑔 ) 𝑥 ) ) ) |
78 |
75
|
oveqd |
⊢ ( ( 𝑣 = ( Base ‘ 𝑔 ) ∧ 𝑎 = ( +g ‘ 𝑔 ) ) → ( ( 𝑟 ( ·𝑠 ‘ 𝑔 ) 𝑤 ) 𝑎 ( 𝑟 ( ·𝑠 ‘ 𝑔 ) 𝑥 ) ) = ( ( 𝑟 ( ·𝑠 ‘ 𝑔 ) 𝑤 ) ( +g ‘ 𝑔 ) ( 𝑟 ( ·𝑠 ‘ 𝑔 ) 𝑥 ) ) ) |
79 |
77 78
|
eqeq12d |
⊢ ( ( 𝑣 = ( Base ‘ 𝑔 ) ∧ 𝑎 = ( +g ‘ 𝑔 ) ) → ( ( 𝑟 ( ·𝑠 ‘ 𝑔 ) ( 𝑤 𝑎 𝑥 ) ) = ( ( 𝑟 ( ·𝑠 ‘ 𝑔 ) 𝑤 ) 𝑎 ( 𝑟 ( ·𝑠 ‘ 𝑔 ) 𝑥 ) ) ↔ ( 𝑟 ( ·𝑠 ‘ 𝑔 ) ( 𝑤 ( +g ‘ 𝑔 ) 𝑥 ) ) = ( ( 𝑟 ( ·𝑠 ‘ 𝑔 ) 𝑤 ) ( +g ‘ 𝑔 ) ( 𝑟 ( ·𝑠 ‘ 𝑔 ) 𝑥 ) ) ) ) |
80 |
75
|
oveqd |
⊢ ( ( 𝑣 = ( Base ‘ 𝑔 ) ∧ 𝑎 = ( +g ‘ 𝑔 ) ) → ( ( 𝑞 ( ·𝑠 ‘ 𝑔 ) 𝑤 ) 𝑎 ( 𝑟 ( ·𝑠 ‘ 𝑔 ) 𝑤 ) ) = ( ( 𝑞 ( ·𝑠 ‘ 𝑔 ) 𝑤 ) ( +g ‘ 𝑔 ) ( 𝑟 ( ·𝑠 ‘ 𝑔 ) 𝑤 ) ) ) |
81 |
80
|
eqeq2d |
⊢ ( ( 𝑣 = ( Base ‘ 𝑔 ) ∧ 𝑎 = ( +g ‘ 𝑔 ) ) → ( ( ( 𝑞 ( +g ‘ ( Scalar ‘ 𝑔 ) ) 𝑟 ) ( ·𝑠 ‘ 𝑔 ) 𝑤 ) = ( ( 𝑞 ( ·𝑠 ‘ 𝑔 ) 𝑤 ) 𝑎 ( 𝑟 ( ·𝑠 ‘ 𝑔 ) 𝑤 ) ) ↔ ( ( 𝑞 ( +g ‘ ( Scalar ‘ 𝑔 ) ) 𝑟 ) ( ·𝑠 ‘ 𝑔 ) 𝑤 ) = ( ( 𝑞 ( ·𝑠 ‘ 𝑔 ) 𝑤 ) ( +g ‘ 𝑔 ) ( 𝑟 ( ·𝑠 ‘ 𝑔 ) 𝑤 ) ) ) ) |
82 |
74 79 81
|
3anbi123d |
⊢ ( ( 𝑣 = ( Base ‘ 𝑔 ) ∧ 𝑎 = ( +g ‘ 𝑔 ) ) → ( ( ( 𝑟 ( ·𝑠 ‘ 𝑔 ) 𝑤 ) ∈ 𝑣 ∧ ( 𝑟 ( ·𝑠 ‘ 𝑔 ) ( 𝑤 𝑎 𝑥 ) ) = ( ( 𝑟 ( ·𝑠 ‘ 𝑔 ) 𝑤 ) 𝑎 ( 𝑟 ( ·𝑠 ‘ 𝑔 ) 𝑥 ) ) ∧ ( ( 𝑞 ( +g ‘ ( Scalar ‘ 𝑔 ) ) 𝑟 ) ( ·𝑠 ‘ 𝑔 ) 𝑤 ) = ( ( 𝑞 ( ·𝑠 ‘ 𝑔 ) 𝑤 ) 𝑎 ( 𝑟 ( ·𝑠 ‘ 𝑔 ) 𝑤 ) ) ) ↔ ( ( 𝑟 ( ·𝑠 ‘ 𝑔 ) 𝑤 ) ∈ ( Base ‘ 𝑔 ) ∧ ( 𝑟 ( ·𝑠 ‘ 𝑔 ) ( 𝑤 ( +g ‘ 𝑔 ) 𝑥 ) ) = ( ( 𝑟 ( ·𝑠 ‘ 𝑔 ) 𝑤 ) ( +g ‘ 𝑔 ) ( 𝑟 ( ·𝑠 ‘ 𝑔 ) 𝑥 ) ) ∧ ( ( 𝑞 ( +g ‘ ( Scalar ‘ 𝑔 ) ) 𝑟 ) ( ·𝑠 ‘ 𝑔 ) 𝑤 ) = ( ( 𝑞 ( ·𝑠 ‘ 𝑔 ) 𝑤 ) ( +g ‘ 𝑔 ) ( 𝑟 ( ·𝑠 ‘ 𝑔 ) 𝑤 ) ) ) ) ) |
83 |
82
|
anbi1d |
⊢ ( ( 𝑣 = ( Base ‘ 𝑔 ) ∧ 𝑎 = ( +g ‘ 𝑔 ) ) → ( ( ( ( 𝑟 ( ·𝑠 ‘ 𝑔 ) 𝑤 ) ∈ 𝑣 ∧ ( 𝑟 ( ·𝑠 ‘ 𝑔 ) ( 𝑤 𝑎 𝑥 ) ) = ( ( 𝑟 ( ·𝑠 ‘ 𝑔 ) 𝑤 ) 𝑎 ( 𝑟 ( ·𝑠 ‘ 𝑔 ) 𝑥 ) ) ∧ ( ( 𝑞 ( +g ‘ ( Scalar ‘ 𝑔 ) ) 𝑟 ) ( ·𝑠 ‘ 𝑔 ) 𝑤 ) = ( ( 𝑞 ( ·𝑠 ‘ 𝑔 ) 𝑤 ) 𝑎 ( 𝑟 ( ·𝑠 ‘ 𝑔 ) 𝑤 ) ) ) ∧ ( ( ( 𝑞 ( .r ‘ ( Scalar ‘ 𝑔 ) ) 𝑟 ) ( ·𝑠 ‘ 𝑔 ) 𝑤 ) = ( 𝑞 ( ·𝑠 ‘ 𝑔 ) ( 𝑟 ( ·𝑠 ‘ 𝑔 ) 𝑤 ) ) ∧ ( ( 1r ‘ ( Scalar ‘ 𝑔 ) ) ( ·𝑠 ‘ 𝑔 ) 𝑤 ) = 𝑤 ∧ ( ( 0g ‘ ( Scalar ‘ 𝑔 ) ) ( ·𝑠 ‘ 𝑔 ) 𝑤 ) = ( 0g ‘ 𝑔 ) ) ) ↔ ( ( ( 𝑟 ( ·𝑠 ‘ 𝑔 ) 𝑤 ) ∈ ( Base ‘ 𝑔 ) ∧ ( 𝑟 ( ·𝑠 ‘ 𝑔 ) ( 𝑤 ( +g ‘ 𝑔 ) 𝑥 ) ) = ( ( 𝑟 ( ·𝑠 ‘ 𝑔 ) 𝑤 ) ( +g ‘ 𝑔 ) ( 𝑟 ( ·𝑠 ‘ 𝑔 ) 𝑥 ) ) ∧ ( ( 𝑞 ( +g ‘ ( Scalar ‘ 𝑔 ) ) 𝑟 ) ( ·𝑠 ‘ 𝑔 ) 𝑤 ) = ( ( 𝑞 ( ·𝑠 ‘ 𝑔 ) 𝑤 ) ( +g ‘ 𝑔 ) ( 𝑟 ( ·𝑠 ‘ 𝑔 ) 𝑤 ) ) ) ∧ ( ( ( 𝑞 ( .r ‘ ( Scalar ‘ 𝑔 ) ) 𝑟 ) ( ·𝑠 ‘ 𝑔 ) 𝑤 ) = ( 𝑞 ( ·𝑠 ‘ 𝑔 ) ( 𝑟 ( ·𝑠 ‘ 𝑔 ) 𝑤 ) ) ∧ ( ( 1r ‘ ( Scalar ‘ 𝑔 ) ) ( ·𝑠 ‘ 𝑔 ) 𝑤 ) = 𝑤 ∧ ( ( 0g ‘ ( Scalar ‘ 𝑔 ) ) ( ·𝑠 ‘ 𝑔 ) 𝑤 ) = ( 0g ‘ 𝑔 ) ) ) ) ) |
84 |
73 83
|
raleqbidv |
⊢ ( ( 𝑣 = ( Base ‘ 𝑔 ) ∧ 𝑎 = ( +g ‘ 𝑔 ) ) → ( ∀ 𝑤 ∈ 𝑣 ( ( ( 𝑟 ( ·𝑠 ‘ 𝑔 ) 𝑤 ) ∈ 𝑣 ∧ ( 𝑟 ( ·𝑠 ‘ 𝑔 ) ( 𝑤 𝑎 𝑥 ) ) = ( ( 𝑟 ( ·𝑠 ‘ 𝑔 ) 𝑤 ) 𝑎 ( 𝑟 ( ·𝑠 ‘ 𝑔 ) 𝑥 ) ) ∧ ( ( 𝑞 ( +g ‘ ( Scalar ‘ 𝑔 ) ) 𝑟 ) ( ·𝑠 ‘ 𝑔 ) 𝑤 ) = ( ( 𝑞 ( ·𝑠 ‘ 𝑔 ) 𝑤 ) 𝑎 ( 𝑟 ( ·𝑠 ‘ 𝑔 ) 𝑤 ) ) ) ∧ ( ( ( 𝑞 ( .r ‘ ( Scalar ‘ 𝑔 ) ) 𝑟 ) ( ·𝑠 ‘ 𝑔 ) 𝑤 ) = ( 𝑞 ( ·𝑠 ‘ 𝑔 ) ( 𝑟 ( ·𝑠 ‘ 𝑔 ) 𝑤 ) ) ∧ ( ( 1r ‘ ( Scalar ‘ 𝑔 ) ) ( ·𝑠 ‘ 𝑔 ) 𝑤 ) = 𝑤 ∧ ( ( 0g ‘ ( Scalar ‘ 𝑔 ) ) ( ·𝑠 ‘ 𝑔 ) 𝑤 ) = ( 0g ‘ 𝑔 ) ) ) ↔ ∀ 𝑤 ∈ ( Base ‘ 𝑔 ) ( ( ( 𝑟 ( ·𝑠 ‘ 𝑔 ) 𝑤 ) ∈ ( Base ‘ 𝑔 ) ∧ ( 𝑟 ( ·𝑠 ‘ 𝑔 ) ( 𝑤 ( +g ‘ 𝑔 ) 𝑥 ) ) = ( ( 𝑟 ( ·𝑠 ‘ 𝑔 ) 𝑤 ) ( +g ‘ 𝑔 ) ( 𝑟 ( ·𝑠 ‘ 𝑔 ) 𝑥 ) ) ∧ ( ( 𝑞 ( +g ‘ ( Scalar ‘ 𝑔 ) ) 𝑟 ) ( ·𝑠 ‘ 𝑔 ) 𝑤 ) = ( ( 𝑞 ( ·𝑠 ‘ 𝑔 ) 𝑤 ) ( +g ‘ 𝑔 ) ( 𝑟 ( ·𝑠 ‘ 𝑔 ) 𝑤 ) ) ) ∧ ( ( ( 𝑞 ( .r ‘ ( Scalar ‘ 𝑔 ) ) 𝑟 ) ( ·𝑠 ‘ 𝑔 ) 𝑤 ) = ( 𝑞 ( ·𝑠 ‘ 𝑔 ) ( 𝑟 ( ·𝑠 ‘ 𝑔 ) 𝑤 ) ) ∧ ( ( 1r ‘ ( Scalar ‘ 𝑔 ) ) ( ·𝑠 ‘ 𝑔 ) 𝑤 ) = 𝑤 ∧ ( ( 0g ‘ ( Scalar ‘ 𝑔 ) ) ( ·𝑠 ‘ 𝑔 ) 𝑤 ) = ( 0g ‘ 𝑔 ) ) ) ) ) |
85 |
73 84
|
raleqbidv |
⊢ ( ( 𝑣 = ( Base ‘ 𝑔 ) ∧ 𝑎 = ( +g ‘ 𝑔 ) ) → ( ∀ 𝑥 ∈ 𝑣 ∀ 𝑤 ∈ 𝑣 ( ( ( 𝑟 ( ·𝑠 ‘ 𝑔 ) 𝑤 ) ∈ 𝑣 ∧ ( 𝑟 ( ·𝑠 ‘ 𝑔 ) ( 𝑤 𝑎 𝑥 ) ) = ( ( 𝑟 ( ·𝑠 ‘ 𝑔 ) 𝑤 ) 𝑎 ( 𝑟 ( ·𝑠 ‘ 𝑔 ) 𝑥 ) ) ∧ ( ( 𝑞 ( +g ‘ ( Scalar ‘ 𝑔 ) ) 𝑟 ) ( ·𝑠 ‘ 𝑔 ) 𝑤 ) = ( ( 𝑞 ( ·𝑠 ‘ 𝑔 ) 𝑤 ) 𝑎 ( 𝑟 ( ·𝑠 ‘ 𝑔 ) 𝑤 ) ) ) ∧ ( ( ( 𝑞 ( .r ‘ ( Scalar ‘ 𝑔 ) ) 𝑟 ) ( ·𝑠 ‘ 𝑔 ) 𝑤 ) = ( 𝑞 ( ·𝑠 ‘ 𝑔 ) ( 𝑟 ( ·𝑠 ‘ 𝑔 ) 𝑤 ) ) ∧ ( ( 1r ‘ ( Scalar ‘ 𝑔 ) ) ( ·𝑠 ‘ 𝑔 ) 𝑤 ) = 𝑤 ∧ ( ( 0g ‘ ( Scalar ‘ 𝑔 ) ) ( ·𝑠 ‘ 𝑔 ) 𝑤 ) = ( 0g ‘ 𝑔 ) ) ) ↔ ∀ 𝑥 ∈ ( Base ‘ 𝑔 ) ∀ 𝑤 ∈ ( Base ‘ 𝑔 ) ( ( ( 𝑟 ( ·𝑠 ‘ 𝑔 ) 𝑤 ) ∈ ( Base ‘ 𝑔 ) ∧ ( 𝑟 ( ·𝑠 ‘ 𝑔 ) ( 𝑤 ( +g ‘ 𝑔 ) 𝑥 ) ) = ( ( 𝑟 ( ·𝑠 ‘ 𝑔 ) 𝑤 ) ( +g ‘ 𝑔 ) ( 𝑟 ( ·𝑠 ‘ 𝑔 ) 𝑥 ) ) ∧ ( ( 𝑞 ( +g ‘ ( Scalar ‘ 𝑔 ) ) 𝑟 ) ( ·𝑠 ‘ 𝑔 ) 𝑤 ) = ( ( 𝑞 ( ·𝑠 ‘ 𝑔 ) 𝑤 ) ( +g ‘ 𝑔 ) ( 𝑟 ( ·𝑠 ‘ 𝑔 ) 𝑤 ) ) ) ∧ ( ( ( 𝑞 ( .r ‘ ( Scalar ‘ 𝑔 ) ) 𝑟 ) ( ·𝑠 ‘ 𝑔 ) 𝑤 ) = ( 𝑞 ( ·𝑠 ‘ 𝑔 ) ( 𝑟 ( ·𝑠 ‘ 𝑔 ) 𝑤 ) ) ∧ ( ( 1r ‘ ( Scalar ‘ 𝑔 ) ) ( ·𝑠 ‘ 𝑔 ) 𝑤 ) = 𝑤 ∧ ( ( 0g ‘ ( Scalar ‘ 𝑔 ) ) ( ·𝑠 ‘ 𝑔 ) 𝑤 ) = ( 0g ‘ 𝑔 ) ) ) ) ) |
86 |
85
|
2ralbidv |
⊢ ( ( 𝑣 = ( Base ‘ 𝑔 ) ∧ 𝑎 = ( +g ‘ 𝑔 ) ) → ( ∀ 𝑞 ∈ ( Base ‘ ( Scalar ‘ 𝑔 ) ) ∀ 𝑟 ∈ ( Base ‘ ( Scalar ‘ 𝑔 ) ) ∀ 𝑥 ∈ 𝑣 ∀ 𝑤 ∈ 𝑣 ( ( ( 𝑟 ( ·𝑠 ‘ 𝑔 ) 𝑤 ) ∈ 𝑣 ∧ ( 𝑟 ( ·𝑠 ‘ 𝑔 ) ( 𝑤 𝑎 𝑥 ) ) = ( ( 𝑟 ( ·𝑠 ‘ 𝑔 ) 𝑤 ) 𝑎 ( 𝑟 ( ·𝑠 ‘ 𝑔 ) 𝑥 ) ) ∧ ( ( 𝑞 ( +g ‘ ( Scalar ‘ 𝑔 ) ) 𝑟 ) ( ·𝑠 ‘ 𝑔 ) 𝑤 ) = ( ( 𝑞 ( ·𝑠 ‘ 𝑔 ) 𝑤 ) 𝑎 ( 𝑟 ( ·𝑠 ‘ 𝑔 ) 𝑤 ) ) ) ∧ ( ( ( 𝑞 ( .r ‘ ( Scalar ‘ 𝑔 ) ) 𝑟 ) ( ·𝑠 ‘ 𝑔 ) 𝑤 ) = ( 𝑞 ( ·𝑠 ‘ 𝑔 ) ( 𝑟 ( ·𝑠 ‘ 𝑔 ) 𝑤 ) ) ∧ ( ( 1r ‘ ( Scalar ‘ 𝑔 ) ) ( ·𝑠 ‘ 𝑔 ) 𝑤 ) = 𝑤 ∧ ( ( 0g ‘ ( Scalar ‘ 𝑔 ) ) ( ·𝑠 ‘ 𝑔 ) 𝑤 ) = ( 0g ‘ 𝑔 ) ) ) ↔ ∀ 𝑞 ∈ ( Base ‘ ( Scalar ‘ 𝑔 ) ) ∀ 𝑟 ∈ ( Base ‘ ( Scalar ‘ 𝑔 ) ) ∀ 𝑥 ∈ ( Base ‘ 𝑔 ) ∀ 𝑤 ∈ ( Base ‘ 𝑔 ) ( ( ( 𝑟 ( ·𝑠 ‘ 𝑔 ) 𝑤 ) ∈ ( Base ‘ 𝑔 ) ∧ ( 𝑟 ( ·𝑠 ‘ 𝑔 ) ( 𝑤 ( +g ‘ 𝑔 ) 𝑥 ) ) = ( ( 𝑟 ( ·𝑠 ‘ 𝑔 ) 𝑤 ) ( +g ‘ 𝑔 ) ( 𝑟 ( ·𝑠 ‘ 𝑔 ) 𝑥 ) ) ∧ ( ( 𝑞 ( +g ‘ ( Scalar ‘ 𝑔 ) ) 𝑟 ) ( ·𝑠 ‘ 𝑔 ) 𝑤 ) = ( ( 𝑞 ( ·𝑠 ‘ 𝑔 ) 𝑤 ) ( +g ‘ 𝑔 ) ( 𝑟 ( ·𝑠 ‘ 𝑔 ) 𝑤 ) ) ) ∧ ( ( ( 𝑞 ( .r ‘ ( Scalar ‘ 𝑔 ) ) 𝑟 ) ( ·𝑠 ‘ 𝑔 ) 𝑤 ) = ( 𝑞 ( ·𝑠 ‘ 𝑔 ) ( 𝑟 ( ·𝑠 ‘ 𝑔 ) 𝑤 ) ) ∧ ( ( 1r ‘ ( Scalar ‘ 𝑔 ) ) ( ·𝑠 ‘ 𝑔 ) 𝑤 ) = 𝑤 ∧ ( ( 0g ‘ ( Scalar ‘ 𝑔 ) ) ( ·𝑠 ‘ 𝑔 ) 𝑤 ) = ( 0g ‘ 𝑔 ) ) ) ) ) |
87 |
86
|
anbi2d |
⊢ ( ( 𝑣 = ( Base ‘ 𝑔 ) ∧ 𝑎 = ( +g ‘ 𝑔 ) ) → ( ( ( Scalar ‘ 𝑔 ) ∈ SRing ∧ ∀ 𝑞 ∈ ( Base ‘ ( Scalar ‘ 𝑔 ) ) ∀ 𝑟 ∈ ( Base ‘ ( Scalar ‘ 𝑔 ) ) ∀ 𝑥 ∈ 𝑣 ∀ 𝑤 ∈ 𝑣 ( ( ( 𝑟 ( ·𝑠 ‘ 𝑔 ) 𝑤 ) ∈ 𝑣 ∧ ( 𝑟 ( ·𝑠 ‘ 𝑔 ) ( 𝑤 𝑎 𝑥 ) ) = ( ( 𝑟 ( ·𝑠 ‘ 𝑔 ) 𝑤 ) 𝑎 ( 𝑟 ( ·𝑠 ‘ 𝑔 ) 𝑥 ) ) ∧ ( ( 𝑞 ( +g ‘ ( Scalar ‘ 𝑔 ) ) 𝑟 ) ( ·𝑠 ‘ 𝑔 ) 𝑤 ) = ( ( 𝑞 ( ·𝑠 ‘ 𝑔 ) 𝑤 ) 𝑎 ( 𝑟 ( ·𝑠 ‘ 𝑔 ) 𝑤 ) ) ) ∧ ( ( ( 𝑞 ( .r ‘ ( Scalar ‘ 𝑔 ) ) 𝑟 ) ( ·𝑠 ‘ 𝑔 ) 𝑤 ) = ( 𝑞 ( ·𝑠 ‘ 𝑔 ) ( 𝑟 ( ·𝑠 ‘ 𝑔 ) 𝑤 ) ) ∧ ( ( 1r ‘ ( Scalar ‘ 𝑔 ) ) ( ·𝑠 ‘ 𝑔 ) 𝑤 ) = 𝑤 ∧ ( ( 0g ‘ ( Scalar ‘ 𝑔 ) ) ( ·𝑠 ‘ 𝑔 ) 𝑤 ) = ( 0g ‘ 𝑔 ) ) ) ) ↔ ( ( Scalar ‘ 𝑔 ) ∈ SRing ∧ ∀ 𝑞 ∈ ( Base ‘ ( Scalar ‘ 𝑔 ) ) ∀ 𝑟 ∈ ( Base ‘ ( Scalar ‘ 𝑔 ) ) ∀ 𝑥 ∈ ( Base ‘ 𝑔 ) ∀ 𝑤 ∈ ( Base ‘ 𝑔 ) ( ( ( 𝑟 ( ·𝑠 ‘ 𝑔 ) 𝑤 ) ∈ ( Base ‘ 𝑔 ) ∧ ( 𝑟 ( ·𝑠 ‘ 𝑔 ) ( 𝑤 ( +g ‘ 𝑔 ) 𝑥 ) ) = ( ( 𝑟 ( ·𝑠 ‘ 𝑔 ) 𝑤 ) ( +g ‘ 𝑔 ) ( 𝑟 ( ·𝑠 ‘ 𝑔 ) 𝑥 ) ) ∧ ( ( 𝑞 ( +g ‘ ( Scalar ‘ 𝑔 ) ) 𝑟 ) ( ·𝑠 ‘ 𝑔 ) 𝑤 ) = ( ( 𝑞 ( ·𝑠 ‘ 𝑔 ) 𝑤 ) ( +g ‘ 𝑔 ) ( 𝑟 ( ·𝑠 ‘ 𝑔 ) 𝑤 ) ) ) ∧ ( ( ( 𝑞 ( .r ‘ ( Scalar ‘ 𝑔 ) ) 𝑟 ) ( ·𝑠 ‘ 𝑔 ) 𝑤 ) = ( 𝑞 ( ·𝑠 ‘ 𝑔 ) ( 𝑟 ( ·𝑠 ‘ 𝑔 ) 𝑤 ) ) ∧ ( ( 1r ‘ ( Scalar ‘ 𝑔 ) ) ( ·𝑠 ‘ 𝑔 ) 𝑤 ) = 𝑤 ∧ ( ( 0g ‘ ( Scalar ‘ 𝑔 ) ) ( ·𝑠 ‘ 𝑔 ) 𝑤 ) = ( 0g ‘ 𝑔 ) ) ) ) ) ) |
88 |
72 87
|
syl5bb |
⊢ ( ( 𝑣 = ( Base ‘ 𝑔 ) ∧ 𝑎 = ( +g ‘ 𝑔 ) ) → ( [ ( ·𝑠 ‘ 𝑔 ) / 𝑠 ] [ ( Scalar ‘ 𝑔 ) / 𝑓 ] [ ( Base ‘ 𝑓 ) / 𝑘 ] [ ( +g ‘ 𝑓 ) / 𝑝 ] [ ( .r ‘ 𝑓 ) / 𝑡 ] ( 𝑓 ∈ SRing ∧ ∀ 𝑞 ∈ 𝑘 ∀ 𝑟 ∈ 𝑘 ∀ 𝑥 ∈ 𝑣 ∀ 𝑤 ∈ 𝑣 ( ( ( 𝑟 𝑠 𝑤 ) ∈ 𝑣 ∧ ( 𝑟 𝑠 ( 𝑤 𝑎 𝑥 ) ) = ( ( 𝑟 𝑠 𝑤 ) 𝑎 ( 𝑟 𝑠 𝑥 ) ) ∧ ( ( 𝑞 𝑝 𝑟 ) 𝑠 𝑤 ) = ( ( 𝑞 𝑠 𝑤 ) 𝑎 ( 𝑟 𝑠 𝑤 ) ) ) ∧ ( ( ( 𝑞 𝑡 𝑟 ) 𝑠 𝑤 ) = ( 𝑞 𝑠 ( 𝑟 𝑠 𝑤 ) ) ∧ ( ( 1r ‘ 𝑓 ) 𝑠 𝑤 ) = 𝑤 ∧ ( ( 0g ‘ 𝑓 ) 𝑠 𝑤 ) = ( 0g ‘ 𝑔 ) ) ) ) ↔ ( ( Scalar ‘ 𝑔 ) ∈ SRing ∧ ∀ 𝑞 ∈ ( Base ‘ ( Scalar ‘ 𝑔 ) ) ∀ 𝑟 ∈ ( Base ‘ ( Scalar ‘ 𝑔 ) ) ∀ 𝑥 ∈ ( Base ‘ 𝑔 ) ∀ 𝑤 ∈ ( Base ‘ 𝑔 ) ( ( ( 𝑟 ( ·𝑠 ‘ 𝑔 ) 𝑤 ) ∈ ( Base ‘ 𝑔 ) ∧ ( 𝑟 ( ·𝑠 ‘ 𝑔 ) ( 𝑤 ( +g ‘ 𝑔 ) 𝑥 ) ) = ( ( 𝑟 ( ·𝑠 ‘ 𝑔 ) 𝑤 ) ( +g ‘ 𝑔 ) ( 𝑟 ( ·𝑠 ‘ 𝑔 ) 𝑥 ) ) ∧ ( ( 𝑞 ( +g ‘ ( Scalar ‘ 𝑔 ) ) 𝑟 ) ( ·𝑠 ‘ 𝑔 ) 𝑤 ) = ( ( 𝑞 ( ·𝑠 ‘ 𝑔 ) 𝑤 ) ( +g ‘ 𝑔 ) ( 𝑟 ( ·𝑠 ‘ 𝑔 ) 𝑤 ) ) ) ∧ ( ( ( 𝑞 ( .r ‘ ( Scalar ‘ 𝑔 ) ) 𝑟 ) ( ·𝑠 ‘ 𝑔 ) 𝑤 ) = ( 𝑞 ( ·𝑠 ‘ 𝑔 ) ( 𝑟 ( ·𝑠 ‘ 𝑔 ) 𝑤 ) ) ∧ ( ( 1r ‘ ( Scalar ‘ 𝑔 ) ) ( ·𝑠 ‘ 𝑔 ) 𝑤 ) = 𝑤 ∧ ( ( 0g ‘ ( Scalar ‘ 𝑔 ) ) ( ·𝑠 ‘ 𝑔 ) 𝑤 ) = ( 0g ‘ 𝑔 ) ) ) ) ) ) |
89 |
11 12 88
|
sbc2ie |
⊢ ( [ ( Base ‘ 𝑔 ) / 𝑣 ] [ ( +g ‘ 𝑔 ) / 𝑎 ] [ ( ·𝑠 ‘ 𝑔 ) / 𝑠 ] [ ( Scalar ‘ 𝑔 ) / 𝑓 ] [ ( Base ‘ 𝑓 ) / 𝑘 ] [ ( +g ‘ 𝑓 ) / 𝑝 ] [ ( .r ‘ 𝑓 ) / 𝑡 ] ( 𝑓 ∈ SRing ∧ ∀ 𝑞 ∈ 𝑘 ∀ 𝑟 ∈ 𝑘 ∀ 𝑥 ∈ 𝑣 ∀ 𝑤 ∈ 𝑣 ( ( ( 𝑟 𝑠 𝑤 ) ∈ 𝑣 ∧ ( 𝑟 𝑠 ( 𝑤 𝑎 𝑥 ) ) = ( ( 𝑟 𝑠 𝑤 ) 𝑎 ( 𝑟 𝑠 𝑥 ) ) ∧ ( ( 𝑞 𝑝 𝑟 ) 𝑠 𝑤 ) = ( ( 𝑞 𝑠 𝑤 ) 𝑎 ( 𝑟 𝑠 𝑤 ) ) ) ∧ ( ( ( 𝑞 𝑡 𝑟 ) 𝑠 𝑤 ) = ( 𝑞 𝑠 ( 𝑟 𝑠 𝑤 ) ) ∧ ( ( 1r ‘ 𝑓 ) 𝑠 𝑤 ) = 𝑤 ∧ ( ( 0g ‘ 𝑓 ) 𝑠 𝑤 ) = ( 0g ‘ 𝑔 ) ) ) ) ↔ ( ( Scalar ‘ 𝑔 ) ∈ SRing ∧ ∀ 𝑞 ∈ ( Base ‘ ( Scalar ‘ 𝑔 ) ) ∀ 𝑟 ∈ ( Base ‘ ( Scalar ‘ 𝑔 ) ) ∀ 𝑥 ∈ ( Base ‘ 𝑔 ) ∀ 𝑤 ∈ ( Base ‘ 𝑔 ) ( ( ( 𝑟 ( ·𝑠 ‘ 𝑔 ) 𝑤 ) ∈ ( Base ‘ 𝑔 ) ∧ ( 𝑟 ( ·𝑠 ‘ 𝑔 ) ( 𝑤 ( +g ‘ 𝑔 ) 𝑥 ) ) = ( ( 𝑟 ( ·𝑠 ‘ 𝑔 ) 𝑤 ) ( +g ‘ 𝑔 ) ( 𝑟 ( ·𝑠 ‘ 𝑔 ) 𝑥 ) ) ∧ ( ( 𝑞 ( +g ‘ ( Scalar ‘ 𝑔 ) ) 𝑟 ) ( ·𝑠 ‘ 𝑔 ) 𝑤 ) = ( ( 𝑞 ( ·𝑠 ‘ 𝑔 ) 𝑤 ) ( +g ‘ 𝑔 ) ( 𝑟 ( ·𝑠 ‘ 𝑔 ) 𝑤 ) ) ) ∧ ( ( ( 𝑞 ( .r ‘ ( Scalar ‘ 𝑔 ) ) 𝑟 ) ( ·𝑠 ‘ 𝑔 ) 𝑤 ) = ( 𝑞 ( ·𝑠 ‘ 𝑔 ) ( 𝑟 ( ·𝑠 ‘ 𝑔 ) 𝑤 ) ) ∧ ( ( 1r ‘ ( Scalar ‘ 𝑔 ) ) ( ·𝑠 ‘ 𝑔 ) 𝑤 ) = 𝑤 ∧ ( ( 0g ‘ ( Scalar ‘ 𝑔 ) ) ( ·𝑠 ‘ 𝑔 ) 𝑤 ) = ( 0g ‘ 𝑔 ) ) ) ) ) |
90 |
|
fveq2 |
⊢ ( 𝑔 = 𝑊 → ( Scalar ‘ 𝑔 ) = ( Scalar ‘ 𝑊 ) ) |
91 |
90 5
|
eqtr4di |
⊢ ( 𝑔 = 𝑊 → ( Scalar ‘ 𝑔 ) = 𝐹 ) |
92 |
91
|
eleq1d |
⊢ ( 𝑔 = 𝑊 → ( ( Scalar ‘ 𝑔 ) ∈ SRing ↔ 𝐹 ∈ SRing ) ) |
93 |
91
|
fveq2d |
⊢ ( 𝑔 = 𝑊 → ( Base ‘ ( Scalar ‘ 𝑔 ) ) = ( Base ‘ 𝐹 ) ) |
94 |
93 6
|
eqtr4di |
⊢ ( 𝑔 = 𝑊 → ( Base ‘ ( Scalar ‘ 𝑔 ) ) = 𝐾 ) |
95 |
|
fveq2 |
⊢ ( 𝑔 = 𝑊 → ( Base ‘ 𝑔 ) = ( Base ‘ 𝑊 ) ) |
96 |
95 1
|
eqtr4di |
⊢ ( 𝑔 = 𝑊 → ( Base ‘ 𝑔 ) = 𝑉 ) |
97 |
|
fveq2 |
⊢ ( 𝑔 = 𝑊 → ( ·𝑠 ‘ 𝑔 ) = ( ·𝑠 ‘ 𝑊 ) ) |
98 |
97 3
|
eqtr4di |
⊢ ( 𝑔 = 𝑊 → ( ·𝑠 ‘ 𝑔 ) = · ) |
99 |
98
|
oveqd |
⊢ ( 𝑔 = 𝑊 → ( 𝑟 ( ·𝑠 ‘ 𝑔 ) 𝑤 ) = ( 𝑟 · 𝑤 ) ) |
100 |
99 96
|
eleq12d |
⊢ ( 𝑔 = 𝑊 → ( ( 𝑟 ( ·𝑠 ‘ 𝑔 ) 𝑤 ) ∈ ( Base ‘ 𝑔 ) ↔ ( 𝑟 · 𝑤 ) ∈ 𝑉 ) ) |
101 |
|
eqidd |
⊢ ( 𝑔 = 𝑊 → 𝑟 = 𝑟 ) |
102 |
|
fveq2 |
⊢ ( 𝑔 = 𝑊 → ( +g ‘ 𝑔 ) = ( +g ‘ 𝑊 ) ) |
103 |
102 2
|
eqtr4di |
⊢ ( 𝑔 = 𝑊 → ( +g ‘ 𝑔 ) = + ) |
104 |
103
|
oveqd |
⊢ ( 𝑔 = 𝑊 → ( 𝑤 ( +g ‘ 𝑔 ) 𝑥 ) = ( 𝑤 + 𝑥 ) ) |
105 |
98 101 104
|
oveq123d |
⊢ ( 𝑔 = 𝑊 → ( 𝑟 ( ·𝑠 ‘ 𝑔 ) ( 𝑤 ( +g ‘ 𝑔 ) 𝑥 ) ) = ( 𝑟 · ( 𝑤 + 𝑥 ) ) ) |
106 |
98
|
oveqd |
⊢ ( 𝑔 = 𝑊 → ( 𝑟 ( ·𝑠 ‘ 𝑔 ) 𝑥 ) = ( 𝑟 · 𝑥 ) ) |
107 |
103 99 106
|
oveq123d |
⊢ ( 𝑔 = 𝑊 → ( ( 𝑟 ( ·𝑠 ‘ 𝑔 ) 𝑤 ) ( +g ‘ 𝑔 ) ( 𝑟 ( ·𝑠 ‘ 𝑔 ) 𝑥 ) ) = ( ( 𝑟 · 𝑤 ) + ( 𝑟 · 𝑥 ) ) ) |
108 |
105 107
|
eqeq12d |
⊢ ( 𝑔 = 𝑊 → ( ( 𝑟 ( ·𝑠 ‘ 𝑔 ) ( 𝑤 ( +g ‘ 𝑔 ) 𝑥 ) ) = ( ( 𝑟 ( ·𝑠 ‘ 𝑔 ) 𝑤 ) ( +g ‘ 𝑔 ) ( 𝑟 ( ·𝑠 ‘ 𝑔 ) 𝑥 ) ) ↔ ( 𝑟 · ( 𝑤 + 𝑥 ) ) = ( ( 𝑟 · 𝑤 ) + ( 𝑟 · 𝑥 ) ) ) ) |
109 |
91
|
fveq2d |
⊢ ( 𝑔 = 𝑊 → ( +g ‘ ( Scalar ‘ 𝑔 ) ) = ( +g ‘ 𝐹 ) ) |
110 |
109 7
|
eqtr4di |
⊢ ( 𝑔 = 𝑊 → ( +g ‘ ( Scalar ‘ 𝑔 ) ) = ⨣ ) |
111 |
110
|
oveqd |
⊢ ( 𝑔 = 𝑊 → ( 𝑞 ( +g ‘ ( Scalar ‘ 𝑔 ) ) 𝑟 ) = ( 𝑞 ⨣ 𝑟 ) ) |
112 |
|
eqidd |
⊢ ( 𝑔 = 𝑊 → 𝑤 = 𝑤 ) |
113 |
98 111 112
|
oveq123d |
⊢ ( 𝑔 = 𝑊 → ( ( 𝑞 ( +g ‘ ( Scalar ‘ 𝑔 ) ) 𝑟 ) ( ·𝑠 ‘ 𝑔 ) 𝑤 ) = ( ( 𝑞 ⨣ 𝑟 ) · 𝑤 ) ) |
114 |
98
|
oveqd |
⊢ ( 𝑔 = 𝑊 → ( 𝑞 ( ·𝑠 ‘ 𝑔 ) 𝑤 ) = ( 𝑞 · 𝑤 ) ) |
115 |
103 114 99
|
oveq123d |
⊢ ( 𝑔 = 𝑊 → ( ( 𝑞 ( ·𝑠 ‘ 𝑔 ) 𝑤 ) ( +g ‘ 𝑔 ) ( 𝑟 ( ·𝑠 ‘ 𝑔 ) 𝑤 ) ) = ( ( 𝑞 · 𝑤 ) + ( 𝑟 · 𝑤 ) ) ) |
116 |
113 115
|
eqeq12d |
⊢ ( 𝑔 = 𝑊 → ( ( ( 𝑞 ( +g ‘ ( Scalar ‘ 𝑔 ) ) 𝑟 ) ( ·𝑠 ‘ 𝑔 ) 𝑤 ) = ( ( 𝑞 ( ·𝑠 ‘ 𝑔 ) 𝑤 ) ( +g ‘ 𝑔 ) ( 𝑟 ( ·𝑠 ‘ 𝑔 ) 𝑤 ) ) ↔ ( ( 𝑞 ⨣ 𝑟 ) · 𝑤 ) = ( ( 𝑞 · 𝑤 ) + ( 𝑟 · 𝑤 ) ) ) ) |
117 |
100 108 116
|
3anbi123d |
⊢ ( 𝑔 = 𝑊 → ( ( ( 𝑟 ( ·𝑠 ‘ 𝑔 ) 𝑤 ) ∈ ( Base ‘ 𝑔 ) ∧ ( 𝑟 ( ·𝑠 ‘ 𝑔 ) ( 𝑤 ( +g ‘ 𝑔 ) 𝑥 ) ) = ( ( 𝑟 ( ·𝑠 ‘ 𝑔 ) 𝑤 ) ( +g ‘ 𝑔 ) ( 𝑟 ( ·𝑠 ‘ 𝑔 ) 𝑥 ) ) ∧ ( ( 𝑞 ( +g ‘ ( Scalar ‘ 𝑔 ) ) 𝑟 ) ( ·𝑠 ‘ 𝑔 ) 𝑤 ) = ( ( 𝑞 ( ·𝑠 ‘ 𝑔 ) 𝑤 ) ( +g ‘ 𝑔 ) ( 𝑟 ( ·𝑠 ‘ 𝑔 ) 𝑤 ) ) ) ↔ ( ( 𝑟 · 𝑤 ) ∈ 𝑉 ∧ ( 𝑟 · ( 𝑤 + 𝑥 ) ) = ( ( 𝑟 · 𝑤 ) + ( 𝑟 · 𝑥 ) ) ∧ ( ( 𝑞 ⨣ 𝑟 ) · 𝑤 ) = ( ( 𝑞 · 𝑤 ) + ( 𝑟 · 𝑤 ) ) ) ) ) |
118 |
91
|
fveq2d |
⊢ ( 𝑔 = 𝑊 → ( .r ‘ ( Scalar ‘ 𝑔 ) ) = ( .r ‘ 𝐹 ) ) |
119 |
118 8
|
eqtr4di |
⊢ ( 𝑔 = 𝑊 → ( .r ‘ ( Scalar ‘ 𝑔 ) ) = × ) |
120 |
119
|
oveqd |
⊢ ( 𝑔 = 𝑊 → ( 𝑞 ( .r ‘ ( Scalar ‘ 𝑔 ) ) 𝑟 ) = ( 𝑞 × 𝑟 ) ) |
121 |
98 120 112
|
oveq123d |
⊢ ( 𝑔 = 𝑊 → ( ( 𝑞 ( .r ‘ ( Scalar ‘ 𝑔 ) ) 𝑟 ) ( ·𝑠 ‘ 𝑔 ) 𝑤 ) = ( ( 𝑞 × 𝑟 ) · 𝑤 ) ) |
122 |
|
eqidd |
⊢ ( 𝑔 = 𝑊 → 𝑞 = 𝑞 ) |
123 |
98 122 99
|
oveq123d |
⊢ ( 𝑔 = 𝑊 → ( 𝑞 ( ·𝑠 ‘ 𝑔 ) ( 𝑟 ( ·𝑠 ‘ 𝑔 ) 𝑤 ) ) = ( 𝑞 · ( 𝑟 · 𝑤 ) ) ) |
124 |
121 123
|
eqeq12d |
⊢ ( 𝑔 = 𝑊 → ( ( ( 𝑞 ( .r ‘ ( Scalar ‘ 𝑔 ) ) 𝑟 ) ( ·𝑠 ‘ 𝑔 ) 𝑤 ) = ( 𝑞 ( ·𝑠 ‘ 𝑔 ) ( 𝑟 ( ·𝑠 ‘ 𝑔 ) 𝑤 ) ) ↔ ( ( 𝑞 × 𝑟 ) · 𝑤 ) = ( 𝑞 · ( 𝑟 · 𝑤 ) ) ) ) |
125 |
91
|
fveq2d |
⊢ ( 𝑔 = 𝑊 → ( 1r ‘ ( Scalar ‘ 𝑔 ) ) = ( 1r ‘ 𝐹 ) ) |
126 |
125 9
|
eqtr4di |
⊢ ( 𝑔 = 𝑊 → ( 1r ‘ ( Scalar ‘ 𝑔 ) ) = 1 ) |
127 |
98 126 112
|
oveq123d |
⊢ ( 𝑔 = 𝑊 → ( ( 1r ‘ ( Scalar ‘ 𝑔 ) ) ( ·𝑠 ‘ 𝑔 ) 𝑤 ) = ( 1 · 𝑤 ) ) |
128 |
127
|
eqeq1d |
⊢ ( 𝑔 = 𝑊 → ( ( ( 1r ‘ ( Scalar ‘ 𝑔 ) ) ( ·𝑠 ‘ 𝑔 ) 𝑤 ) = 𝑤 ↔ ( 1 · 𝑤 ) = 𝑤 ) ) |
129 |
91
|
fveq2d |
⊢ ( 𝑔 = 𝑊 → ( 0g ‘ ( Scalar ‘ 𝑔 ) ) = ( 0g ‘ 𝐹 ) ) |
130 |
129 10
|
eqtr4di |
⊢ ( 𝑔 = 𝑊 → ( 0g ‘ ( Scalar ‘ 𝑔 ) ) = 𝑂 ) |
131 |
98 130 112
|
oveq123d |
⊢ ( 𝑔 = 𝑊 → ( ( 0g ‘ ( Scalar ‘ 𝑔 ) ) ( ·𝑠 ‘ 𝑔 ) 𝑤 ) = ( 𝑂 · 𝑤 ) ) |
132 |
|
fveq2 |
⊢ ( 𝑔 = 𝑊 → ( 0g ‘ 𝑔 ) = ( 0g ‘ 𝑊 ) ) |
133 |
132 4
|
eqtr4di |
⊢ ( 𝑔 = 𝑊 → ( 0g ‘ 𝑔 ) = 0 ) |
134 |
131 133
|
eqeq12d |
⊢ ( 𝑔 = 𝑊 → ( ( ( 0g ‘ ( Scalar ‘ 𝑔 ) ) ( ·𝑠 ‘ 𝑔 ) 𝑤 ) = ( 0g ‘ 𝑔 ) ↔ ( 𝑂 · 𝑤 ) = 0 ) ) |
135 |
124 128 134
|
3anbi123d |
⊢ ( 𝑔 = 𝑊 → ( ( ( ( 𝑞 ( .r ‘ ( Scalar ‘ 𝑔 ) ) 𝑟 ) ( ·𝑠 ‘ 𝑔 ) 𝑤 ) = ( 𝑞 ( ·𝑠 ‘ 𝑔 ) ( 𝑟 ( ·𝑠 ‘ 𝑔 ) 𝑤 ) ) ∧ ( ( 1r ‘ ( Scalar ‘ 𝑔 ) ) ( ·𝑠 ‘ 𝑔 ) 𝑤 ) = 𝑤 ∧ ( ( 0g ‘ ( Scalar ‘ 𝑔 ) ) ( ·𝑠 ‘ 𝑔 ) 𝑤 ) = ( 0g ‘ 𝑔 ) ) ↔ ( ( ( 𝑞 × 𝑟 ) · 𝑤 ) = ( 𝑞 · ( 𝑟 · 𝑤 ) ) ∧ ( 1 · 𝑤 ) = 𝑤 ∧ ( 𝑂 · 𝑤 ) = 0 ) ) ) |
136 |
117 135
|
anbi12d |
⊢ ( 𝑔 = 𝑊 → ( ( ( ( 𝑟 ( ·𝑠 ‘ 𝑔 ) 𝑤 ) ∈ ( Base ‘ 𝑔 ) ∧ ( 𝑟 ( ·𝑠 ‘ 𝑔 ) ( 𝑤 ( +g ‘ 𝑔 ) 𝑥 ) ) = ( ( 𝑟 ( ·𝑠 ‘ 𝑔 ) 𝑤 ) ( +g ‘ 𝑔 ) ( 𝑟 ( ·𝑠 ‘ 𝑔 ) 𝑥 ) ) ∧ ( ( 𝑞 ( +g ‘ ( Scalar ‘ 𝑔 ) ) 𝑟 ) ( ·𝑠 ‘ 𝑔 ) 𝑤 ) = ( ( 𝑞 ( ·𝑠 ‘ 𝑔 ) 𝑤 ) ( +g ‘ 𝑔 ) ( 𝑟 ( ·𝑠 ‘ 𝑔 ) 𝑤 ) ) ) ∧ ( ( ( 𝑞 ( .r ‘ ( Scalar ‘ 𝑔 ) ) 𝑟 ) ( ·𝑠 ‘ 𝑔 ) 𝑤 ) = ( 𝑞 ( ·𝑠 ‘ 𝑔 ) ( 𝑟 ( ·𝑠 ‘ 𝑔 ) 𝑤 ) ) ∧ ( ( 1r ‘ ( Scalar ‘ 𝑔 ) ) ( ·𝑠 ‘ 𝑔 ) 𝑤 ) = 𝑤 ∧ ( ( 0g ‘ ( Scalar ‘ 𝑔 ) ) ( ·𝑠 ‘ 𝑔 ) 𝑤 ) = ( 0g ‘ 𝑔 ) ) ) ↔ ( ( ( 𝑟 · 𝑤 ) ∈ 𝑉 ∧ ( 𝑟 · ( 𝑤 + 𝑥 ) ) = ( ( 𝑟 · 𝑤 ) + ( 𝑟 · 𝑥 ) ) ∧ ( ( 𝑞 ⨣ 𝑟 ) · 𝑤 ) = ( ( 𝑞 · 𝑤 ) + ( 𝑟 · 𝑤 ) ) ) ∧ ( ( ( 𝑞 × 𝑟 ) · 𝑤 ) = ( 𝑞 · ( 𝑟 · 𝑤 ) ) ∧ ( 1 · 𝑤 ) = 𝑤 ∧ ( 𝑂 · 𝑤 ) = 0 ) ) ) ) |
137 |
96 136
|
raleqbidv |
⊢ ( 𝑔 = 𝑊 → ( ∀ 𝑤 ∈ ( Base ‘ 𝑔 ) ( ( ( 𝑟 ( ·𝑠 ‘ 𝑔 ) 𝑤 ) ∈ ( Base ‘ 𝑔 ) ∧ ( 𝑟 ( ·𝑠 ‘ 𝑔 ) ( 𝑤 ( +g ‘ 𝑔 ) 𝑥 ) ) = ( ( 𝑟 ( ·𝑠 ‘ 𝑔 ) 𝑤 ) ( +g ‘ 𝑔 ) ( 𝑟 ( ·𝑠 ‘ 𝑔 ) 𝑥 ) ) ∧ ( ( 𝑞 ( +g ‘ ( Scalar ‘ 𝑔 ) ) 𝑟 ) ( ·𝑠 ‘ 𝑔 ) 𝑤 ) = ( ( 𝑞 ( ·𝑠 ‘ 𝑔 ) 𝑤 ) ( +g ‘ 𝑔 ) ( 𝑟 ( ·𝑠 ‘ 𝑔 ) 𝑤 ) ) ) ∧ ( ( ( 𝑞 ( .r ‘ ( Scalar ‘ 𝑔 ) ) 𝑟 ) ( ·𝑠 ‘ 𝑔 ) 𝑤 ) = ( 𝑞 ( ·𝑠 ‘ 𝑔 ) ( 𝑟 ( ·𝑠 ‘ 𝑔 ) 𝑤 ) ) ∧ ( ( 1r ‘ ( Scalar ‘ 𝑔 ) ) ( ·𝑠 ‘ 𝑔 ) 𝑤 ) = 𝑤 ∧ ( ( 0g ‘ ( Scalar ‘ 𝑔 ) ) ( ·𝑠 ‘ 𝑔 ) 𝑤 ) = ( 0g ‘ 𝑔 ) ) ) ↔ ∀ 𝑤 ∈ 𝑉 ( ( ( 𝑟 · 𝑤 ) ∈ 𝑉 ∧ ( 𝑟 · ( 𝑤 + 𝑥 ) ) = ( ( 𝑟 · 𝑤 ) + ( 𝑟 · 𝑥 ) ) ∧ ( ( 𝑞 ⨣ 𝑟 ) · 𝑤 ) = ( ( 𝑞 · 𝑤 ) + ( 𝑟 · 𝑤 ) ) ) ∧ ( ( ( 𝑞 × 𝑟 ) · 𝑤 ) = ( 𝑞 · ( 𝑟 · 𝑤 ) ) ∧ ( 1 · 𝑤 ) = 𝑤 ∧ ( 𝑂 · 𝑤 ) = 0 ) ) ) ) |
138 |
96 137
|
raleqbidv |
⊢ ( 𝑔 = 𝑊 → ( ∀ 𝑥 ∈ ( Base ‘ 𝑔 ) ∀ 𝑤 ∈ ( Base ‘ 𝑔 ) ( ( ( 𝑟 ( ·𝑠 ‘ 𝑔 ) 𝑤 ) ∈ ( Base ‘ 𝑔 ) ∧ ( 𝑟 ( ·𝑠 ‘ 𝑔 ) ( 𝑤 ( +g ‘ 𝑔 ) 𝑥 ) ) = ( ( 𝑟 ( ·𝑠 ‘ 𝑔 ) 𝑤 ) ( +g ‘ 𝑔 ) ( 𝑟 ( ·𝑠 ‘ 𝑔 ) 𝑥 ) ) ∧ ( ( 𝑞 ( +g ‘ ( Scalar ‘ 𝑔 ) ) 𝑟 ) ( ·𝑠 ‘ 𝑔 ) 𝑤 ) = ( ( 𝑞 ( ·𝑠 ‘ 𝑔 ) 𝑤 ) ( +g ‘ 𝑔 ) ( 𝑟 ( ·𝑠 ‘ 𝑔 ) 𝑤 ) ) ) ∧ ( ( ( 𝑞 ( .r ‘ ( Scalar ‘ 𝑔 ) ) 𝑟 ) ( ·𝑠 ‘ 𝑔 ) 𝑤 ) = ( 𝑞 ( ·𝑠 ‘ 𝑔 ) ( 𝑟 ( ·𝑠 ‘ 𝑔 ) 𝑤 ) ) ∧ ( ( 1r ‘ ( Scalar ‘ 𝑔 ) ) ( ·𝑠 ‘ 𝑔 ) 𝑤 ) = 𝑤 ∧ ( ( 0g ‘ ( Scalar ‘ 𝑔 ) ) ( ·𝑠 ‘ 𝑔 ) 𝑤 ) = ( 0g ‘ 𝑔 ) ) ) ↔ ∀ 𝑥 ∈ 𝑉 ∀ 𝑤 ∈ 𝑉 ( ( ( 𝑟 · 𝑤 ) ∈ 𝑉 ∧ ( 𝑟 · ( 𝑤 + 𝑥 ) ) = ( ( 𝑟 · 𝑤 ) + ( 𝑟 · 𝑥 ) ) ∧ ( ( 𝑞 ⨣ 𝑟 ) · 𝑤 ) = ( ( 𝑞 · 𝑤 ) + ( 𝑟 · 𝑤 ) ) ) ∧ ( ( ( 𝑞 × 𝑟 ) · 𝑤 ) = ( 𝑞 · ( 𝑟 · 𝑤 ) ) ∧ ( 1 · 𝑤 ) = 𝑤 ∧ ( 𝑂 · 𝑤 ) = 0 ) ) ) ) |
139 |
94 138
|
raleqbidv |
⊢ ( 𝑔 = 𝑊 → ( ∀ 𝑟 ∈ ( Base ‘ ( Scalar ‘ 𝑔 ) ) ∀ 𝑥 ∈ ( Base ‘ 𝑔 ) ∀ 𝑤 ∈ ( Base ‘ 𝑔 ) ( ( ( 𝑟 ( ·𝑠 ‘ 𝑔 ) 𝑤 ) ∈ ( Base ‘ 𝑔 ) ∧ ( 𝑟 ( ·𝑠 ‘ 𝑔 ) ( 𝑤 ( +g ‘ 𝑔 ) 𝑥 ) ) = ( ( 𝑟 ( ·𝑠 ‘ 𝑔 ) 𝑤 ) ( +g ‘ 𝑔 ) ( 𝑟 ( ·𝑠 ‘ 𝑔 ) 𝑥 ) ) ∧ ( ( 𝑞 ( +g ‘ ( Scalar ‘ 𝑔 ) ) 𝑟 ) ( ·𝑠 ‘ 𝑔 ) 𝑤 ) = ( ( 𝑞 ( ·𝑠 ‘ 𝑔 ) 𝑤 ) ( +g ‘ 𝑔 ) ( 𝑟 ( ·𝑠 ‘ 𝑔 ) 𝑤 ) ) ) ∧ ( ( ( 𝑞 ( .r ‘ ( Scalar ‘ 𝑔 ) ) 𝑟 ) ( ·𝑠 ‘ 𝑔 ) 𝑤 ) = ( 𝑞 ( ·𝑠 ‘ 𝑔 ) ( 𝑟 ( ·𝑠 ‘ 𝑔 ) 𝑤 ) ) ∧ ( ( 1r ‘ ( Scalar ‘ 𝑔 ) ) ( ·𝑠 ‘ 𝑔 ) 𝑤 ) = 𝑤 ∧ ( ( 0g ‘ ( Scalar ‘ 𝑔 ) ) ( ·𝑠 ‘ 𝑔 ) 𝑤 ) = ( 0g ‘ 𝑔 ) ) ) ↔ ∀ 𝑟 ∈ 𝐾 ∀ 𝑥 ∈ 𝑉 ∀ 𝑤 ∈ 𝑉 ( ( ( 𝑟 · 𝑤 ) ∈ 𝑉 ∧ ( 𝑟 · ( 𝑤 + 𝑥 ) ) = ( ( 𝑟 · 𝑤 ) + ( 𝑟 · 𝑥 ) ) ∧ ( ( 𝑞 ⨣ 𝑟 ) · 𝑤 ) = ( ( 𝑞 · 𝑤 ) + ( 𝑟 · 𝑤 ) ) ) ∧ ( ( ( 𝑞 × 𝑟 ) · 𝑤 ) = ( 𝑞 · ( 𝑟 · 𝑤 ) ) ∧ ( 1 · 𝑤 ) = 𝑤 ∧ ( 𝑂 · 𝑤 ) = 0 ) ) ) ) |
140 |
94 139
|
raleqbidv |
⊢ ( 𝑔 = 𝑊 → ( ∀ 𝑞 ∈ ( Base ‘ ( Scalar ‘ 𝑔 ) ) ∀ 𝑟 ∈ ( Base ‘ ( Scalar ‘ 𝑔 ) ) ∀ 𝑥 ∈ ( Base ‘ 𝑔 ) ∀ 𝑤 ∈ ( Base ‘ 𝑔 ) ( ( ( 𝑟 ( ·𝑠 ‘ 𝑔 ) 𝑤 ) ∈ ( Base ‘ 𝑔 ) ∧ ( 𝑟 ( ·𝑠 ‘ 𝑔 ) ( 𝑤 ( +g ‘ 𝑔 ) 𝑥 ) ) = ( ( 𝑟 ( ·𝑠 ‘ 𝑔 ) 𝑤 ) ( +g ‘ 𝑔 ) ( 𝑟 ( ·𝑠 ‘ 𝑔 ) 𝑥 ) ) ∧ ( ( 𝑞 ( +g ‘ ( Scalar ‘ 𝑔 ) ) 𝑟 ) ( ·𝑠 ‘ 𝑔 ) 𝑤 ) = ( ( 𝑞 ( ·𝑠 ‘ 𝑔 ) 𝑤 ) ( +g ‘ 𝑔 ) ( 𝑟 ( ·𝑠 ‘ 𝑔 ) 𝑤 ) ) ) ∧ ( ( ( 𝑞 ( .r ‘ ( Scalar ‘ 𝑔 ) ) 𝑟 ) ( ·𝑠 ‘ 𝑔 ) 𝑤 ) = ( 𝑞 ( ·𝑠 ‘ 𝑔 ) ( 𝑟 ( ·𝑠 ‘ 𝑔 ) 𝑤 ) ) ∧ ( ( 1r ‘ ( Scalar ‘ 𝑔 ) ) ( ·𝑠 ‘ 𝑔 ) 𝑤 ) = 𝑤 ∧ ( ( 0g ‘ ( Scalar ‘ 𝑔 ) ) ( ·𝑠 ‘ 𝑔 ) 𝑤 ) = ( 0g ‘ 𝑔 ) ) ) ↔ ∀ 𝑞 ∈ 𝐾 ∀ 𝑟 ∈ 𝐾 ∀ 𝑥 ∈ 𝑉 ∀ 𝑤 ∈ 𝑉 ( ( ( 𝑟 · 𝑤 ) ∈ 𝑉 ∧ ( 𝑟 · ( 𝑤 + 𝑥 ) ) = ( ( 𝑟 · 𝑤 ) + ( 𝑟 · 𝑥 ) ) ∧ ( ( 𝑞 ⨣ 𝑟 ) · 𝑤 ) = ( ( 𝑞 · 𝑤 ) + ( 𝑟 · 𝑤 ) ) ) ∧ ( ( ( 𝑞 × 𝑟 ) · 𝑤 ) = ( 𝑞 · ( 𝑟 · 𝑤 ) ) ∧ ( 1 · 𝑤 ) = 𝑤 ∧ ( 𝑂 · 𝑤 ) = 0 ) ) ) ) |
141 |
92 140
|
anbi12d |
⊢ ( 𝑔 = 𝑊 → ( ( ( Scalar ‘ 𝑔 ) ∈ SRing ∧ ∀ 𝑞 ∈ ( Base ‘ ( Scalar ‘ 𝑔 ) ) ∀ 𝑟 ∈ ( Base ‘ ( Scalar ‘ 𝑔 ) ) ∀ 𝑥 ∈ ( Base ‘ 𝑔 ) ∀ 𝑤 ∈ ( Base ‘ 𝑔 ) ( ( ( 𝑟 ( ·𝑠 ‘ 𝑔 ) 𝑤 ) ∈ ( Base ‘ 𝑔 ) ∧ ( 𝑟 ( ·𝑠 ‘ 𝑔 ) ( 𝑤 ( +g ‘ 𝑔 ) 𝑥 ) ) = ( ( 𝑟 ( ·𝑠 ‘ 𝑔 ) 𝑤 ) ( +g ‘ 𝑔 ) ( 𝑟 ( ·𝑠 ‘ 𝑔 ) 𝑥 ) ) ∧ ( ( 𝑞 ( +g ‘ ( Scalar ‘ 𝑔 ) ) 𝑟 ) ( ·𝑠 ‘ 𝑔 ) 𝑤 ) = ( ( 𝑞 ( ·𝑠 ‘ 𝑔 ) 𝑤 ) ( +g ‘ 𝑔 ) ( 𝑟 ( ·𝑠 ‘ 𝑔 ) 𝑤 ) ) ) ∧ ( ( ( 𝑞 ( .r ‘ ( Scalar ‘ 𝑔 ) ) 𝑟 ) ( ·𝑠 ‘ 𝑔 ) 𝑤 ) = ( 𝑞 ( ·𝑠 ‘ 𝑔 ) ( 𝑟 ( ·𝑠 ‘ 𝑔 ) 𝑤 ) ) ∧ ( ( 1r ‘ ( Scalar ‘ 𝑔 ) ) ( ·𝑠 ‘ 𝑔 ) 𝑤 ) = 𝑤 ∧ ( ( 0g ‘ ( Scalar ‘ 𝑔 ) ) ( ·𝑠 ‘ 𝑔 ) 𝑤 ) = ( 0g ‘ 𝑔 ) ) ) ) ↔ ( 𝐹 ∈ SRing ∧ ∀ 𝑞 ∈ 𝐾 ∀ 𝑟 ∈ 𝐾 ∀ 𝑥 ∈ 𝑉 ∀ 𝑤 ∈ 𝑉 ( ( ( 𝑟 · 𝑤 ) ∈ 𝑉 ∧ ( 𝑟 · ( 𝑤 + 𝑥 ) ) = ( ( 𝑟 · 𝑤 ) + ( 𝑟 · 𝑥 ) ) ∧ ( ( 𝑞 ⨣ 𝑟 ) · 𝑤 ) = ( ( 𝑞 · 𝑤 ) + ( 𝑟 · 𝑤 ) ) ) ∧ ( ( ( 𝑞 × 𝑟 ) · 𝑤 ) = ( 𝑞 · ( 𝑟 · 𝑤 ) ) ∧ ( 1 · 𝑤 ) = 𝑤 ∧ ( 𝑂 · 𝑤 ) = 0 ) ) ) ) ) |
142 |
89 141
|
syl5bb |
⊢ ( 𝑔 = 𝑊 → ( [ ( Base ‘ 𝑔 ) / 𝑣 ] [ ( +g ‘ 𝑔 ) / 𝑎 ] [ ( ·𝑠 ‘ 𝑔 ) / 𝑠 ] [ ( Scalar ‘ 𝑔 ) / 𝑓 ] [ ( Base ‘ 𝑓 ) / 𝑘 ] [ ( +g ‘ 𝑓 ) / 𝑝 ] [ ( .r ‘ 𝑓 ) / 𝑡 ] ( 𝑓 ∈ SRing ∧ ∀ 𝑞 ∈ 𝑘 ∀ 𝑟 ∈ 𝑘 ∀ 𝑥 ∈ 𝑣 ∀ 𝑤 ∈ 𝑣 ( ( ( 𝑟 𝑠 𝑤 ) ∈ 𝑣 ∧ ( 𝑟 𝑠 ( 𝑤 𝑎 𝑥 ) ) = ( ( 𝑟 𝑠 𝑤 ) 𝑎 ( 𝑟 𝑠 𝑥 ) ) ∧ ( ( 𝑞 𝑝 𝑟 ) 𝑠 𝑤 ) = ( ( 𝑞 𝑠 𝑤 ) 𝑎 ( 𝑟 𝑠 𝑤 ) ) ) ∧ ( ( ( 𝑞 𝑡 𝑟 ) 𝑠 𝑤 ) = ( 𝑞 𝑠 ( 𝑟 𝑠 𝑤 ) ) ∧ ( ( 1r ‘ 𝑓 ) 𝑠 𝑤 ) = 𝑤 ∧ ( ( 0g ‘ 𝑓 ) 𝑠 𝑤 ) = ( 0g ‘ 𝑔 ) ) ) ) ↔ ( 𝐹 ∈ SRing ∧ ∀ 𝑞 ∈ 𝐾 ∀ 𝑟 ∈ 𝐾 ∀ 𝑥 ∈ 𝑉 ∀ 𝑤 ∈ 𝑉 ( ( ( 𝑟 · 𝑤 ) ∈ 𝑉 ∧ ( 𝑟 · ( 𝑤 + 𝑥 ) ) = ( ( 𝑟 · 𝑤 ) + ( 𝑟 · 𝑥 ) ) ∧ ( ( 𝑞 ⨣ 𝑟 ) · 𝑤 ) = ( ( 𝑞 · 𝑤 ) + ( 𝑟 · 𝑤 ) ) ) ∧ ( ( ( 𝑞 × 𝑟 ) · 𝑤 ) = ( 𝑞 · ( 𝑟 · 𝑤 ) ) ∧ ( 1 · 𝑤 ) = 𝑤 ∧ ( 𝑂 · 𝑤 ) = 0 ) ) ) ) ) |
143 |
|
df-slmd |
⊢ SLMod = { 𝑔 ∈ CMnd ∣ [ ( Base ‘ 𝑔 ) / 𝑣 ] [ ( +g ‘ 𝑔 ) / 𝑎 ] [ ( ·𝑠 ‘ 𝑔 ) / 𝑠 ] [ ( Scalar ‘ 𝑔 ) / 𝑓 ] [ ( Base ‘ 𝑓 ) / 𝑘 ] [ ( +g ‘ 𝑓 ) / 𝑝 ] [ ( .r ‘ 𝑓 ) / 𝑡 ] ( 𝑓 ∈ SRing ∧ ∀ 𝑞 ∈ 𝑘 ∀ 𝑟 ∈ 𝑘 ∀ 𝑥 ∈ 𝑣 ∀ 𝑤 ∈ 𝑣 ( ( ( 𝑟 𝑠 𝑤 ) ∈ 𝑣 ∧ ( 𝑟 𝑠 ( 𝑤 𝑎 𝑥 ) ) = ( ( 𝑟 𝑠 𝑤 ) 𝑎 ( 𝑟 𝑠 𝑥 ) ) ∧ ( ( 𝑞 𝑝 𝑟 ) 𝑠 𝑤 ) = ( ( 𝑞 𝑠 𝑤 ) 𝑎 ( 𝑟 𝑠 𝑤 ) ) ) ∧ ( ( ( 𝑞 𝑡 𝑟 ) 𝑠 𝑤 ) = ( 𝑞 𝑠 ( 𝑟 𝑠 𝑤 ) ) ∧ ( ( 1r ‘ 𝑓 ) 𝑠 𝑤 ) = 𝑤 ∧ ( ( 0g ‘ 𝑓 ) 𝑠 𝑤 ) = ( 0g ‘ 𝑔 ) ) ) ) } |
144 |
142 143
|
elrab2 |
⊢ ( 𝑊 ∈ SLMod ↔ ( 𝑊 ∈ CMnd ∧ ( 𝐹 ∈ SRing ∧ ∀ 𝑞 ∈ 𝐾 ∀ 𝑟 ∈ 𝐾 ∀ 𝑥 ∈ 𝑉 ∀ 𝑤 ∈ 𝑉 ( ( ( 𝑟 · 𝑤 ) ∈ 𝑉 ∧ ( 𝑟 · ( 𝑤 + 𝑥 ) ) = ( ( 𝑟 · 𝑤 ) + ( 𝑟 · 𝑥 ) ) ∧ ( ( 𝑞 ⨣ 𝑟 ) · 𝑤 ) = ( ( 𝑞 · 𝑤 ) + ( 𝑟 · 𝑤 ) ) ) ∧ ( ( ( 𝑞 × 𝑟 ) · 𝑤 ) = ( 𝑞 · ( 𝑟 · 𝑤 ) ) ∧ ( 1 · 𝑤 ) = 𝑤 ∧ ( 𝑂 · 𝑤 ) = 0 ) ) ) ) ) |
145 |
|
3anass |
⊢ ( ( 𝑊 ∈ CMnd ∧ 𝐹 ∈ SRing ∧ ∀ 𝑞 ∈ 𝐾 ∀ 𝑟 ∈ 𝐾 ∀ 𝑥 ∈ 𝑉 ∀ 𝑤 ∈ 𝑉 ( ( ( 𝑟 · 𝑤 ) ∈ 𝑉 ∧ ( 𝑟 · ( 𝑤 + 𝑥 ) ) = ( ( 𝑟 · 𝑤 ) + ( 𝑟 · 𝑥 ) ) ∧ ( ( 𝑞 ⨣ 𝑟 ) · 𝑤 ) = ( ( 𝑞 · 𝑤 ) + ( 𝑟 · 𝑤 ) ) ) ∧ ( ( ( 𝑞 × 𝑟 ) · 𝑤 ) = ( 𝑞 · ( 𝑟 · 𝑤 ) ) ∧ ( 1 · 𝑤 ) = 𝑤 ∧ ( 𝑂 · 𝑤 ) = 0 ) ) ) ↔ ( 𝑊 ∈ CMnd ∧ ( 𝐹 ∈ SRing ∧ ∀ 𝑞 ∈ 𝐾 ∀ 𝑟 ∈ 𝐾 ∀ 𝑥 ∈ 𝑉 ∀ 𝑤 ∈ 𝑉 ( ( ( 𝑟 · 𝑤 ) ∈ 𝑉 ∧ ( 𝑟 · ( 𝑤 + 𝑥 ) ) = ( ( 𝑟 · 𝑤 ) + ( 𝑟 · 𝑥 ) ) ∧ ( ( 𝑞 ⨣ 𝑟 ) · 𝑤 ) = ( ( 𝑞 · 𝑤 ) + ( 𝑟 · 𝑤 ) ) ) ∧ ( ( ( 𝑞 × 𝑟 ) · 𝑤 ) = ( 𝑞 · ( 𝑟 · 𝑤 ) ) ∧ ( 1 · 𝑤 ) = 𝑤 ∧ ( 𝑂 · 𝑤 ) = 0 ) ) ) ) ) |
146 |
144 145
|
bitr4i |
⊢ ( 𝑊 ∈ SLMod ↔ ( 𝑊 ∈ CMnd ∧ 𝐹 ∈ SRing ∧ ∀ 𝑞 ∈ 𝐾 ∀ 𝑟 ∈ 𝐾 ∀ 𝑥 ∈ 𝑉 ∀ 𝑤 ∈ 𝑉 ( ( ( 𝑟 · 𝑤 ) ∈ 𝑉 ∧ ( 𝑟 · ( 𝑤 + 𝑥 ) ) = ( ( 𝑟 · 𝑤 ) + ( 𝑟 · 𝑥 ) ) ∧ ( ( 𝑞 ⨣ 𝑟 ) · 𝑤 ) = ( ( 𝑞 · 𝑤 ) + ( 𝑟 · 𝑤 ) ) ) ∧ ( ( ( 𝑞 × 𝑟 ) · 𝑤 ) = ( 𝑞 · ( 𝑟 · 𝑤 ) ) ∧ ( 1 · 𝑤 ) = 𝑤 ∧ ( 𝑂 · 𝑤 ) = 0 ) ) ) ) |