| Step | Hyp | Ref
| Expression |
| 1 | | prdsinvlem.n |
. . 3
⊢ 𝑁 = (𝑦 ∈ 𝐼 ↦ ((invg‘(𝑅‘𝑦))‘(𝐹‘𝑦))) |
| 2 | | prdsinvlem.r |
. . . . . . 7
⊢ (𝜑 → 𝑅:𝐼⟶Grp) |
| 3 | 2 | ffvelcdmda 7104 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐼) → (𝑅‘𝑦) ∈ Grp) |
| 4 | | prdsinvlem.y |
. . . . . . 7
⊢ 𝑌 = (𝑆Xs𝑅) |
| 5 | | prdsinvlem.b |
. . . . . . 7
⊢ 𝐵 = (Base‘𝑌) |
| 6 | | prdsinvlem.s |
. . . . . . . 8
⊢ (𝜑 → 𝑆 ∈ 𝑉) |
| 7 | 6 | adantr 480 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐼) → 𝑆 ∈ 𝑉) |
| 8 | | prdsinvlem.i |
. . . . . . . 8
⊢ (𝜑 → 𝐼 ∈ 𝑊) |
| 9 | 8 | adantr 480 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐼) → 𝐼 ∈ 𝑊) |
| 10 | 2 | ffnd 6737 |
. . . . . . . 8
⊢ (𝜑 → 𝑅 Fn 𝐼) |
| 11 | 10 | adantr 480 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐼) → 𝑅 Fn 𝐼) |
| 12 | | prdsinvlem.f |
. . . . . . . 8
⊢ (𝜑 → 𝐹 ∈ 𝐵) |
| 13 | 12 | adantr 480 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐼) → 𝐹 ∈ 𝐵) |
| 14 | | simpr 484 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐼) → 𝑦 ∈ 𝐼) |
| 15 | 4, 5, 7, 9, 11, 13, 14 | prdsbasprj 17517 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐼) → (𝐹‘𝑦) ∈ (Base‘(𝑅‘𝑦))) |
| 16 | | eqid 2737 |
. . . . . . 7
⊢
(Base‘(𝑅‘𝑦)) = (Base‘(𝑅‘𝑦)) |
| 17 | | eqid 2737 |
. . . . . . 7
⊢
(invg‘(𝑅‘𝑦)) = (invg‘(𝑅‘𝑦)) |
| 18 | 16, 17 | grpinvcl 19005 |
. . . . . 6
⊢ (((𝑅‘𝑦) ∈ Grp ∧ (𝐹‘𝑦) ∈ (Base‘(𝑅‘𝑦))) → ((invg‘(𝑅‘𝑦))‘(𝐹‘𝑦)) ∈ (Base‘(𝑅‘𝑦))) |
| 19 | 3, 15, 18 | syl2anc 584 |
. . . . 5
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐼) → ((invg‘(𝑅‘𝑦))‘(𝐹‘𝑦)) ∈ (Base‘(𝑅‘𝑦))) |
| 20 | 19 | ralrimiva 3146 |
. . . 4
⊢ (𝜑 → ∀𝑦 ∈ 𝐼 ((invg‘(𝑅‘𝑦))‘(𝐹‘𝑦)) ∈ (Base‘(𝑅‘𝑦))) |
| 21 | 4, 5, 6, 8, 10 | prdsbasmpt 17515 |
. . . 4
⊢ (𝜑 → ((𝑦 ∈ 𝐼 ↦ ((invg‘(𝑅‘𝑦))‘(𝐹‘𝑦))) ∈ 𝐵 ↔ ∀𝑦 ∈ 𝐼 ((invg‘(𝑅‘𝑦))‘(𝐹‘𝑦)) ∈ (Base‘(𝑅‘𝑦)))) |
| 22 | 20, 21 | mpbird 257 |
. . 3
⊢ (𝜑 → (𝑦 ∈ 𝐼 ↦ ((invg‘(𝑅‘𝑦))‘(𝐹‘𝑦))) ∈ 𝐵) |
| 23 | 1, 22 | eqeltrid 2845 |
. 2
⊢ (𝜑 → 𝑁 ∈ 𝐵) |
| 24 | 2 | ffvelcdmda 7104 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐼) → (𝑅‘𝑥) ∈ Grp) |
| 25 | 6 | adantr 480 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐼) → 𝑆 ∈ 𝑉) |
| 26 | 8 | adantr 480 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐼) → 𝐼 ∈ 𝑊) |
| 27 | 10 | adantr 480 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐼) → 𝑅 Fn 𝐼) |
| 28 | 12 | adantr 480 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐼) → 𝐹 ∈ 𝐵) |
| 29 | | simpr 484 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐼) → 𝑥 ∈ 𝐼) |
| 30 | 4, 5, 25, 26, 27, 28, 29 | prdsbasprj 17517 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐼) → (𝐹‘𝑥) ∈ (Base‘(𝑅‘𝑥))) |
| 31 | | eqid 2737 |
. . . . . . 7
⊢
(Base‘(𝑅‘𝑥)) = (Base‘(𝑅‘𝑥)) |
| 32 | | eqid 2737 |
. . . . . . 7
⊢
(+g‘(𝑅‘𝑥)) = (+g‘(𝑅‘𝑥)) |
| 33 | | eqid 2737 |
. . . . . . 7
⊢
(0g‘(𝑅‘𝑥)) = (0g‘(𝑅‘𝑥)) |
| 34 | | eqid 2737 |
. . . . . . 7
⊢
(invg‘(𝑅‘𝑥)) = (invg‘(𝑅‘𝑥)) |
| 35 | 31, 32, 33, 34 | grplinv 19007 |
. . . . . 6
⊢ (((𝑅‘𝑥) ∈ Grp ∧ (𝐹‘𝑥) ∈ (Base‘(𝑅‘𝑥))) → (((invg‘(𝑅‘𝑥))‘(𝐹‘𝑥))(+g‘(𝑅‘𝑥))(𝐹‘𝑥)) = (0g‘(𝑅‘𝑥))) |
| 36 | 24, 30, 35 | syl2anc 584 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐼) → (((invg‘(𝑅‘𝑥))‘(𝐹‘𝑥))(+g‘(𝑅‘𝑥))(𝐹‘𝑥)) = (0g‘(𝑅‘𝑥))) |
| 37 | | 2fveq3 6911 |
. . . . . . . . 9
⊢ (𝑦 = 𝑥 → (invg‘(𝑅‘𝑦)) = (invg‘(𝑅‘𝑥))) |
| 38 | | fveq2 6906 |
. . . . . . . . 9
⊢ (𝑦 = 𝑥 → (𝐹‘𝑦) = (𝐹‘𝑥)) |
| 39 | 37, 38 | fveq12d 6913 |
. . . . . . . 8
⊢ (𝑦 = 𝑥 → ((invg‘(𝑅‘𝑦))‘(𝐹‘𝑦)) = ((invg‘(𝑅‘𝑥))‘(𝐹‘𝑥))) |
| 40 | | fvex 6919 |
. . . . . . . 8
⊢
((invg‘(𝑅‘𝑥))‘(𝐹‘𝑥)) ∈ V |
| 41 | 39, 1, 40 | fvmpt 7016 |
. . . . . . 7
⊢ (𝑥 ∈ 𝐼 → (𝑁‘𝑥) = ((invg‘(𝑅‘𝑥))‘(𝐹‘𝑥))) |
| 42 | 41 | adantl 481 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐼) → (𝑁‘𝑥) = ((invg‘(𝑅‘𝑥))‘(𝐹‘𝑥))) |
| 43 | 42 | oveq1d 7446 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐼) → ((𝑁‘𝑥)(+g‘(𝑅‘𝑥))(𝐹‘𝑥)) = (((invg‘(𝑅‘𝑥))‘(𝐹‘𝑥))(+g‘(𝑅‘𝑥))(𝐹‘𝑥))) |
| 44 | | prdsinvlem.z |
. . . . . . 7
⊢ 0 =
(0g ∘ 𝑅) |
| 45 | 44 | fveq1i 6907 |
. . . . . 6
⊢ ( 0 ‘𝑥) = ((0g ∘
𝑅)‘𝑥) |
| 46 | | fvco2 7006 |
. . . . . . 7
⊢ ((𝑅 Fn 𝐼 ∧ 𝑥 ∈ 𝐼) → ((0g ∘ 𝑅)‘𝑥) = (0g‘(𝑅‘𝑥))) |
| 47 | 10, 46 | sylan 580 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐼) → ((0g ∘ 𝑅)‘𝑥) = (0g‘(𝑅‘𝑥))) |
| 48 | 45, 47 | eqtrid 2789 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐼) → ( 0 ‘𝑥) = (0g‘(𝑅‘𝑥))) |
| 49 | 36, 43, 48 | 3eqtr4d 2787 |
. . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐼) → ((𝑁‘𝑥)(+g‘(𝑅‘𝑥))(𝐹‘𝑥)) = ( 0 ‘𝑥)) |
| 50 | 49 | mpteq2dva 5242 |
. . 3
⊢ (𝜑 → (𝑥 ∈ 𝐼 ↦ ((𝑁‘𝑥)(+g‘(𝑅‘𝑥))(𝐹‘𝑥))) = (𝑥 ∈ 𝐼 ↦ ( 0 ‘𝑥))) |
| 51 | | prdsinvlem.p |
. . . 4
⊢ + =
(+g‘𝑌) |
| 52 | 4, 5, 6, 8, 10, 23, 12, 51 | prdsplusgval 17518 |
. . 3
⊢ (𝜑 → (𝑁 + 𝐹) = (𝑥 ∈ 𝐼 ↦ ((𝑁‘𝑥)(+g‘(𝑅‘𝑥))(𝐹‘𝑥)))) |
| 53 | | fn0g 18676 |
. . . . . 6
⊢
0g Fn V |
| 54 | | ssv 4008 |
. . . . . . 7
⊢ ran 𝑅 ⊆ V |
| 55 | 54 | a1i 11 |
. . . . . 6
⊢ (𝜑 → ran 𝑅 ⊆ V) |
| 56 | | fnco 6686 |
. . . . . 6
⊢
((0g Fn V ∧ 𝑅 Fn 𝐼 ∧ ran 𝑅 ⊆ V) → (0g ∘
𝑅) Fn 𝐼) |
| 57 | 53, 10, 55, 56 | mp3an2i 1468 |
. . . . 5
⊢ (𝜑 → (0g ∘
𝑅) Fn 𝐼) |
| 58 | 44 | fneq1i 6665 |
. . . . 5
⊢ ( 0 Fn 𝐼 ↔ (0g ∘
𝑅) Fn 𝐼) |
| 59 | 57, 58 | sylibr 234 |
. . . 4
⊢ (𝜑 → 0 Fn 𝐼) |
| 60 | | dffn5 6967 |
. . . 4
⊢ ( 0 Fn 𝐼 ↔ 0 = (𝑥 ∈ 𝐼 ↦ ( 0 ‘𝑥))) |
| 61 | 59, 60 | sylib 218 |
. . 3
⊢ (𝜑 → 0 = (𝑥 ∈ 𝐼 ↦ ( 0 ‘𝑥))) |
| 62 | 50, 52, 61 | 3eqtr4d 2787 |
. 2
⊢ (𝜑 → (𝑁 + 𝐹) = 0 ) |
| 63 | 23, 62 | jca 511 |
1
⊢ (𝜑 → (𝑁 ∈ 𝐵 ∧ (𝑁 + 𝐹) = 0 )) |