Step |
Hyp |
Ref |
Expression |
1 |
|
islindf5.f |
⊢ 𝐹 = ( 𝑅 freeLMod 𝐼 ) |
2 |
|
islindf5.b |
⊢ 𝐵 = ( Base ‘ 𝐹 ) |
3 |
|
islindf5.c |
⊢ 𝐶 = ( Base ‘ 𝑇 ) |
4 |
|
islindf5.v |
⊢ · = ( ·𝑠 ‘ 𝑇 ) |
5 |
|
islindf5.e |
⊢ 𝐸 = ( 𝑥 ∈ 𝐵 ↦ ( 𝑇 Σg ( 𝑥 ∘f · 𝐴 ) ) ) |
6 |
|
islindf5.t |
⊢ ( 𝜑 → 𝑇 ∈ LMod ) |
7 |
|
islindf5.i |
⊢ ( 𝜑 → 𝐼 ∈ 𝑋 ) |
8 |
|
islindf5.r |
⊢ ( 𝜑 → 𝑅 = ( Scalar ‘ 𝑇 ) ) |
9 |
|
islindf5.a |
⊢ ( 𝜑 → 𝐴 : 𝐼 ⟶ 𝐶 ) |
10 |
|
eqid |
⊢ ( Scalar ‘ 𝑇 ) = ( Scalar ‘ 𝑇 ) |
11 |
|
eqid |
⊢ ( 0g ‘ 𝑇 ) = ( 0g ‘ 𝑇 ) |
12 |
|
eqid |
⊢ ( 0g ‘ ( Scalar ‘ 𝑇 ) ) = ( 0g ‘ ( Scalar ‘ 𝑇 ) ) |
13 |
|
eqid |
⊢ ( Base ‘ ( ( Scalar ‘ 𝑇 ) freeLMod 𝐼 ) ) = ( Base ‘ ( ( Scalar ‘ 𝑇 ) freeLMod 𝐼 ) ) |
14 |
3 10 4 11 12 13
|
islindf4 |
⊢ ( ( 𝑇 ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐴 : 𝐼 ⟶ 𝐶 ) → ( 𝐴 LIndF 𝑇 ↔ ∀ 𝑦 ∈ ( Base ‘ ( ( Scalar ‘ 𝑇 ) freeLMod 𝐼 ) ) ( ( 𝑇 Σg ( 𝑦 ∘f · 𝐴 ) ) = ( 0g ‘ 𝑇 ) → 𝑦 = ( 𝐼 × { ( 0g ‘ ( Scalar ‘ 𝑇 ) ) } ) ) ) ) |
15 |
6 7 9 14
|
syl3anc |
⊢ ( 𝜑 → ( 𝐴 LIndF 𝑇 ↔ ∀ 𝑦 ∈ ( Base ‘ ( ( Scalar ‘ 𝑇 ) freeLMod 𝐼 ) ) ( ( 𝑇 Σg ( 𝑦 ∘f · 𝐴 ) ) = ( 0g ‘ 𝑇 ) → 𝑦 = ( 𝐼 × { ( 0g ‘ ( Scalar ‘ 𝑇 ) ) } ) ) ) ) |
16 |
|
oveq1 |
⊢ ( 𝑥 = 𝑦 → ( 𝑥 ∘f · 𝐴 ) = ( 𝑦 ∘f · 𝐴 ) ) |
17 |
16
|
oveq2d |
⊢ ( 𝑥 = 𝑦 → ( 𝑇 Σg ( 𝑥 ∘f · 𝐴 ) ) = ( 𝑇 Σg ( 𝑦 ∘f · 𝐴 ) ) ) |
18 |
|
ovex |
⊢ ( 𝑇 Σg ( 𝑦 ∘f · 𝐴 ) ) ∈ V |
19 |
17 5 18
|
fvmpt |
⊢ ( 𝑦 ∈ 𝐵 → ( 𝐸 ‘ 𝑦 ) = ( 𝑇 Σg ( 𝑦 ∘f · 𝐴 ) ) ) |
20 |
19
|
adantl |
⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝐵 ) → ( 𝐸 ‘ 𝑦 ) = ( 𝑇 Σg ( 𝑦 ∘f · 𝐴 ) ) ) |
21 |
20
|
eqeq1d |
⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝐵 ) → ( ( 𝐸 ‘ 𝑦 ) = ( 0g ‘ 𝑇 ) ↔ ( 𝑇 Σg ( 𝑦 ∘f · 𝐴 ) ) = ( 0g ‘ 𝑇 ) ) ) |
22 |
10
|
lmodring |
⊢ ( 𝑇 ∈ LMod → ( Scalar ‘ 𝑇 ) ∈ Ring ) |
23 |
6 22
|
syl |
⊢ ( 𝜑 → ( Scalar ‘ 𝑇 ) ∈ Ring ) |
24 |
8 23
|
eqeltrd |
⊢ ( 𝜑 → 𝑅 ∈ Ring ) |
25 |
|
eqid |
⊢ ( 0g ‘ 𝑅 ) = ( 0g ‘ 𝑅 ) |
26 |
1 25
|
frlm0 |
⊢ ( ( 𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑋 ) → ( 𝐼 × { ( 0g ‘ 𝑅 ) } ) = ( 0g ‘ 𝐹 ) ) |
27 |
24 7 26
|
syl2anc |
⊢ ( 𝜑 → ( 𝐼 × { ( 0g ‘ 𝑅 ) } ) = ( 0g ‘ 𝐹 ) ) |
28 |
8
|
fveq2d |
⊢ ( 𝜑 → ( 0g ‘ 𝑅 ) = ( 0g ‘ ( Scalar ‘ 𝑇 ) ) ) |
29 |
28
|
sneqd |
⊢ ( 𝜑 → { ( 0g ‘ 𝑅 ) } = { ( 0g ‘ ( Scalar ‘ 𝑇 ) ) } ) |
30 |
29
|
xpeq2d |
⊢ ( 𝜑 → ( 𝐼 × { ( 0g ‘ 𝑅 ) } ) = ( 𝐼 × { ( 0g ‘ ( Scalar ‘ 𝑇 ) ) } ) ) |
31 |
27 30
|
eqtr3d |
⊢ ( 𝜑 → ( 0g ‘ 𝐹 ) = ( 𝐼 × { ( 0g ‘ ( Scalar ‘ 𝑇 ) ) } ) ) |
32 |
31
|
adantr |
⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝐵 ) → ( 0g ‘ 𝐹 ) = ( 𝐼 × { ( 0g ‘ ( Scalar ‘ 𝑇 ) ) } ) ) |
33 |
32
|
eqeq2d |
⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝐵 ) → ( 𝑦 = ( 0g ‘ 𝐹 ) ↔ 𝑦 = ( 𝐼 × { ( 0g ‘ ( Scalar ‘ 𝑇 ) ) } ) ) ) |
34 |
21 33
|
imbi12d |
⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝐵 ) → ( ( ( 𝐸 ‘ 𝑦 ) = ( 0g ‘ 𝑇 ) → 𝑦 = ( 0g ‘ 𝐹 ) ) ↔ ( ( 𝑇 Σg ( 𝑦 ∘f · 𝐴 ) ) = ( 0g ‘ 𝑇 ) → 𝑦 = ( 𝐼 × { ( 0g ‘ ( Scalar ‘ 𝑇 ) ) } ) ) ) ) |
35 |
34
|
ralbidva |
⊢ ( 𝜑 → ( ∀ 𝑦 ∈ 𝐵 ( ( 𝐸 ‘ 𝑦 ) = ( 0g ‘ 𝑇 ) → 𝑦 = ( 0g ‘ 𝐹 ) ) ↔ ∀ 𝑦 ∈ 𝐵 ( ( 𝑇 Σg ( 𝑦 ∘f · 𝐴 ) ) = ( 0g ‘ 𝑇 ) → 𝑦 = ( 𝐼 × { ( 0g ‘ ( Scalar ‘ 𝑇 ) ) } ) ) ) ) |
36 |
8
|
eqcomd |
⊢ ( 𝜑 → ( Scalar ‘ 𝑇 ) = 𝑅 ) |
37 |
36
|
oveq1d |
⊢ ( 𝜑 → ( ( Scalar ‘ 𝑇 ) freeLMod 𝐼 ) = ( 𝑅 freeLMod 𝐼 ) ) |
38 |
37 1
|
eqtr4di |
⊢ ( 𝜑 → ( ( Scalar ‘ 𝑇 ) freeLMod 𝐼 ) = 𝐹 ) |
39 |
38
|
fveq2d |
⊢ ( 𝜑 → ( Base ‘ ( ( Scalar ‘ 𝑇 ) freeLMod 𝐼 ) ) = ( Base ‘ 𝐹 ) ) |
40 |
39 2
|
eqtr4di |
⊢ ( 𝜑 → ( Base ‘ ( ( Scalar ‘ 𝑇 ) freeLMod 𝐼 ) ) = 𝐵 ) |
41 |
40
|
raleqdv |
⊢ ( 𝜑 → ( ∀ 𝑦 ∈ ( Base ‘ ( ( Scalar ‘ 𝑇 ) freeLMod 𝐼 ) ) ( ( 𝑇 Σg ( 𝑦 ∘f · 𝐴 ) ) = ( 0g ‘ 𝑇 ) → 𝑦 = ( 𝐼 × { ( 0g ‘ ( Scalar ‘ 𝑇 ) ) } ) ) ↔ ∀ 𝑦 ∈ 𝐵 ( ( 𝑇 Σg ( 𝑦 ∘f · 𝐴 ) ) = ( 0g ‘ 𝑇 ) → 𝑦 = ( 𝐼 × { ( 0g ‘ ( Scalar ‘ 𝑇 ) ) } ) ) ) ) |
42 |
35 41
|
bitr4d |
⊢ ( 𝜑 → ( ∀ 𝑦 ∈ 𝐵 ( ( 𝐸 ‘ 𝑦 ) = ( 0g ‘ 𝑇 ) → 𝑦 = ( 0g ‘ 𝐹 ) ) ↔ ∀ 𝑦 ∈ ( Base ‘ ( ( Scalar ‘ 𝑇 ) freeLMod 𝐼 ) ) ( ( 𝑇 Σg ( 𝑦 ∘f · 𝐴 ) ) = ( 0g ‘ 𝑇 ) → 𝑦 = ( 𝐼 × { ( 0g ‘ ( Scalar ‘ 𝑇 ) ) } ) ) ) ) |
43 |
15 42
|
bitr4d |
⊢ ( 𝜑 → ( 𝐴 LIndF 𝑇 ↔ ∀ 𝑦 ∈ 𝐵 ( ( 𝐸 ‘ 𝑦 ) = ( 0g ‘ 𝑇 ) → 𝑦 = ( 0g ‘ 𝐹 ) ) ) ) |
44 |
1 2 3 4 5 6 7 8 9
|
frlmup1 |
⊢ ( 𝜑 → 𝐸 ∈ ( 𝐹 LMHom 𝑇 ) ) |
45 |
|
lmghm |
⊢ ( 𝐸 ∈ ( 𝐹 LMHom 𝑇 ) → 𝐸 ∈ ( 𝐹 GrpHom 𝑇 ) ) |
46 |
|
eqid |
⊢ ( 0g ‘ 𝐹 ) = ( 0g ‘ 𝐹 ) |
47 |
2 3 46 11
|
ghmf1 |
⊢ ( 𝐸 ∈ ( 𝐹 GrpHom 𝑇 ) → ( 𝐸 : 𝐵 –1-1→ 𝐶 ↔ ∀ 𝑦 ∈ 𝐵 ( ( 𝐸 ‘ 𝑦 ) = ( 0g ‘ 𝑇 ) → 𝑦 = ( 0g ‘ 𝐹 ) ) ) ) |
48 |
44 45 47
|
3syl |
⊢ ( 𝜑 → ( 𝐸 : 𝐵 –1-1→ 𝐶 ↔ ∀ 𝑦 ∈ 𝐵 ( ( 𝐸 ‘ 𝑦 ) = ( 0g ‘ 𝑇 ) → 𝑦 = ( 0g ‘ 𝐹 ) ) ) ) |
49 |
43 48
|
bitr4d |
⊢ ( 𝜑 → ( 𝐴 LIndF 𝑇 ↔ 𝐸 : 𝐵 –1-1→ 𝐶 ) ) |