Step | Hyp | Ref
| Expression |
1 | | prdsinvlem.n |
. . 3
⊢ 𝑁 = (𝑦 ∈ 𝐼 ↦ ((invg‘(𝑅‘𝑦))‘(𝐹‘𝑦))) |
2 | | prdsinvlem.r |
. . . . . . 7
⊢ (𝜑 → 𝑅:𝐼⟶Grp) |
3 | 2 | ffvelrnda 6359 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐼) → (𝑅‘𝑦) ∈ Grp) |
4 | | prdsinvlem.y |
. . . . . . 7
⊢ 𝑌 = (𝑆Xs𝑅) |
5 | | prdsinvlem.b |
. . . . . . 7
⊢ 𝐵 = (Base‘𝑌) |
6 | | prdsinvlem.s |
. . . . . . . 8
⊢ (𝜑 → 𝑆 ∈ 𝑉) |
7 | 6 | adantr 481 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐼) → 𝑆 ∈ 𝑉) |
8 | | prdsinvlem.i |
. . . . . . . 8
⊢ (𝜑 → 𝐼 ∈ 𝑊) |
9 | 8 | adantr 481 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐼) → 𝐼 ∈ 𝑊) |
10 | | ffn 6045 |
. . . . . . . . 9
⊢ (𝑅:𝐼⟶Grp → 𝑅 Fn 𝐼) |
11 | 2, 10 | syl 17 |
. . . . . . . 8
⊢ (𝜑 → 𝑅 Fn 𝐼) |
12 | 11 | adantr 481 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐼) → 𝑅 Fn 𝐼) |
13 | | prdsinvlem.f |
. . . . . . . 8
⊢ (𝜑 → 𝐹 ∈ 𝐵) |
14 | 13 | adantr 481 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐼) → 𝐹 ∈ 𝐵) |
15 | | simpr 477 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐼) → 𝑦 ∈ 𝐼) |
16 | 4, 5, 7, 9, 12, 14, 15 | prdsbasprj 16132 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐼) → (𝐹‘𝑦) ∈ (Base‘(𝑅‘𝑦))) |
17 | | eqid 2622 |
. . . . . . 7
⊢
(Base‘(𝑅‘𝑦)) = (Base‘(𝑅‘𝑦)) |
18 | | eqid 2622 |
. . . . . . 7
⊢
(invg‘(𝑅‘𝑦)) = (invg‘(𝑅‘𝑦)) |
19 | 17, 18 | grpinvcl 17467 |
. . . . . 6
⊢ (((𝑅‘𝑦) ∈ Grp ∧ (𝐹‘𝑦) ∈ (Base‘(𝑅‘𝑦))) → ((invg‘(𝑅‘𝑦))‘(𝐹‘𝑦)) ∈ (Base‘(𝑅‘𝑦))) |
20 | 3, 16, 19 | syl2anc 693 |
. . . . 5
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐼) → ((invg‘(𝑅‘𝑦))‘(𝐹‘𝑦)) ∈ (Base‘(𝑅‘𝑦))) |
21 | 20 | ralrimiva 2966 |
. . . 4
⊢ (𝜑 → ∀𝑦 ∈ 𝐼 ((invg‘(𝑅‘𝑦))‘(𝐹‘𝑦)) ∈ (Base‘(𝑅‘𝑦))) |
22 | 4, 5, 6, 8, 11 | prdsbasmpt 16130 |
. . . 4
⊢ (𝜑 → ((𝑦 ∈ 𝐼 ↦ ((invg‘(𝑅‘𝑦))‘(𝐹‘𝑦))) ∈ 𝐵 ↔ ∀𝑦 ∈ 𝐼 ((invg‘(𝑅‘𝑦))‘(𝐹‘𝑦)) ∈ (Base‘(𝑅‘𝑦)))) |
23 | 21, 22 | mpbird 247 |
. . 3
⊢ (𝜑 → (𝑦 ∈ 𝐼 ↦ ((invg‘(𝑅‘𝑦))‘(𝐹‘𝑦))) ∈ 𝐵) |
24 | 1, 23 | syl5eqel 2705 |
. 2
⊢ (𝜑 → 𝑁 ∈ 𝐵) |
25 | 2 | ffvelrnda 6359 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐼) → (𝑅‘𝑥) ∈ Grp) |
26 | 6 | adantr 481 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐼) → 𝑆 ∈ 𝑉) |
27 | 8 | adantr 481 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐼) → 𝐼 ∈ 𝑊) |
28 | 11 | adantr 481 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐼) → 𝑅 Fn 𝐼) |
29 | 13 | adantr 481 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐼) → 𝐹 ∈ 𝐵) |
30 | | simpr 477 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐼) → 𝑥 ∈ 𝐼) |
31 | 4, 5, 26, 27, 28, 29, 30 | prdsbasprj 16132 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐼) → (𝐹‘𝑥) ∈ (Base‘(𝑅‘𝑥))) |
32 | | eqid 2622 |
. . . . . . 7
⊢
(Base‘(𝑅‘𝑥)) = (Base‘(𝑅‘𝑥)) |
33 | | eqid 2622 |
. . . . . . 7
⊢
(+g‘(𝑅‘𝑥)) = (+g‘(𝑅‘𝑥)) |
34 | | eqid 2622 |
. . . . . . 7
⊢
(0g‘(𝑅‘𝑥)) = (0g‘(𝑅‘𝑥)) |
35 | | eqid 2622 |
. . . . . . 7
⊢
(invg‘(𝑅‘𝑥)) = (invg‘(𝑅‘𝑥)) |
36 | 32, 33, 34, 35 | grplinv 17468 |
. . . . . 6
⊢ (((𝑅‘𝑥) ∈ Grp ∧ (𝐹‘𝑥) ∈ (Base‘(𝑅‘𝑥))) → (((invg‘(𝑅‘𝑥))‘(𝐹‘𝑥))(+g‘(𝑅‘𝑥))(𝐹‘𝑥)) = (0g‘(𝑅‘𝑥))) |
37 | 25, 31, 36 | syl2anc 693 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐼) → (((invg‘(𝑅‘𝑥))‘(𝐹‘𝑥))(+g‘(𝑅‘𝑥))(𝐹‘𝑥)) = (0g‘(𝑅‘𝑥))) |
38 | | fveq2 6191 |
. . . . . . . . . 10
⊢ (𝑦 = 𝑥 → (𝑅‘𝑦) = (𝑅‘𝑥)) |
39 | 38 | fveq2d 6195 |
. . . . . . . . 9
⊢ (𝑦 = 𝑥 → (invg‘(𝑅‘𝑦)) = (invg‘(𝑅‘𝑥))) |
40 | | fveq2 6191 |
. . . . . . . . 9
⊢ (𝑦 = 𝑥 → (𝐹‘𝑦) = (𝐹‘𝑥)) |
41 | 39, 40 | fveq12d 6197 |
. . . . . . . 8
⊢ (𝑦 = 𝑥 → ((invg‘(𝑅‘𝑦))‘(𝐹‘𝑦)) = ((invg‘(𝑅‘𝑥))‘(𝐹‘𝑥))) |
42 | | fvex 6201 |
. . . . . . . 8
⊢
((invg‘(𝑅‘𝑥))‘(𝐹‘𝑥)) ∈ V |
43 | 41, 1, 42 | fvmpt 6282 |
. . . . . . 7
⊢ (𝑥 ∈ 𝐼 → (𝑁‘𝑥) = ((invg‘(𝑅‘𝑥))‘(𝐹‘𝑥))) |
44 | 43 | adantl 482 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐼) → (𝑁‘𝑥) = ((invg‘(𝑅‘𝑥))‘(𝐹‘𝑥))) |
45 | 44 | oveq1d 6665 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐼) → ((𝑁‘𝑥)(+g‘(𝑅‘𝑥))(𝐹‘𝑥)) = (((invg‘(𝑅‘𝑥))‘(𝐹‘𝑥))(+g‘(𝑅‘𝑥))(𝐹‘𝑥))) |
46 | | prdsinvlem.z |
. . . . . . 7
⊢ 0 =
(0g ∘ 𝑅) |
47 | 46 | fveq1i 6192 |
. . . . . 6
⊢ ( 0 ‘𝑥) = ((0g ∘
𝑅)‘𝑥) |
48 | | fvco2 6273 |
. . . . . . 7
⊢ ((𝑅 Fn 𝐼 ∧ 𝑥 ∈ 𝐼) → ((0g ∘ 𝑅)‘𝑥) = (0g‘(𝑅‘𝑥))) |
49 | 11, 48 | sylan 488 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐼) → ((0g ∘ 𝑅)‘𝑥) = (0g‘(𝑅‘𝑥))) |
50 | 47, 49 | syl5eq 2668 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐼) → ( 0 ‘𝑥) = (0g‘(𝑅‘𝑥))) |
51 | 37, 45, 50 | 3eqtr4d 2666 |
. . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐼) → ((𝑁‘𝑥)(+g‘(𝑅‘𝑥))(𝐹‘𝑥)) = ( 0 ‘𝑥)) |
52 | 51 | mpteq2dva 4744 |
. . 3
⊢ (𝜑 → (𝑥 ∈ 𝐼 ↦ ((𝑁‘𝑥)(+g‘(𝑅‘𝑥))(𝐹‘𝑥))) = (𝑥 ∈ 𝐼 ↦ ( 0 ‘𝑥))) |
53 | | prdsinvlem.p |
. . . 4
⊢ + =
(+g‘𝑌) |
54 | 4, 5, 6, 8, 11, 24, 13, 53 | prdsplusgval 16133 |
. . 3
⊢ (𝜑 → (𝑁 + 𝐹) = (𝑥 ∈ 𝐼 ↦ ((𝑁‘𝑥)(+g‘(𝑅‘𝑥))(𝐹‘𝑥)))) |
55 | | fn0g 17262 |
. . . . . . 7
⊢
0g Fn V |
56 | 55 | a1i 11 |
. . . . . 6
⊢ (𝜑 → 0g Fn
V) |
57 | | ssv 3625 |
. . . . . . 7
⊢ ran 𝑅 ⊆ V |
58 | 57 | a1i 11 |
. . . . . 6
⊢ (𝜑 → ran 𝑅 ⊆ V) |
59 | | fnco 5999 |
. . . . . 6
⊢
((0g Fn V ∧ 𝑅 Fn 𝐼 ∧ ran 𝑅 ⊆ V) → (0g ∘
𝑅) Fn 𝐼) |
60 | 56, 11, 58, 59 | syl3anc 1326 |
. . . . 5
⊢ (𝜑 → (0g ∘
𝑅) Fn 𝐼) |
61 | 46 | fneq1i 5985 |
. . . . 5
⊢ ( 0 Fn 𝐼 ↔ (0g ∘
𝑅) Fn 𝐼) |
62 | 60, 61 | sylibr 224 |
. . . 4
⊢ (𝜑 → 0 Fn 𝐼) |
63 | | dffn5 6241 |
. . . 4
⊢ ( 0 Fn 𝐼 ↔ 0 = (𝑥 ∈ 𝐼 ↦ ( 0 ‘𝑥))) |
64 | 62, 63 | sylib 208 |
. . 3
⊢ (𝜑 → 0 = (𝑥 ∈ 𝐼 ↦ ( 0 ‘𝑥))) |
65 | 52, 54, 64 | 3eqtr4d 2666 |
. 2
⊢ (𝜑 → (𝑁 + 𝐹) = 0 ) |
66 | 24, 65 | jca 554 |
1
⊢ (𝜑 → (𝑁 ∈ 𝐵 ∧ (𝑁 + 𝐹) = 0 )) |