Step | Hyp | Ref
| Expression |
1 | | elxp2 5614 |
. . 3
⊢ (𝐴 ∈ (𝐼 × 2o) ↔ ∃𝑎 ∈ 𝐼 ∃𝑏 ∈ 2o 𝐴 = 〈𝑎, 𝑏〉) |
2 | | frgpuptinv.m |
. . . . . . . . . 10
⊢ 𝑀 = (𝑦 ∈ 𝐼, 𝑧 ∈ 2o ↦ 〈𝑦, (1o ∖ 𝑧)〉) |
3 | 2 | efgmval 19329 |
. . . . . . . . 9
⊢ ((𝑎 ∈ 𝐼 ∧ 𝑏 ∈ 2o) → (𝑎𝑀𝑏) = 〈𝑎, (1o ∖ 𝑏)〉) |
4 | 3 | adantl 482 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑎 ∈ 𝐼 ∧ 𝑏 ∈ 2o)) → (𝑎𝑀𝑏) = 〈𝑎, (1o ∖ 𝑏)〉) |
5 | 4 | fveq2d 6775 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑎 ∈ 𝐼 ∧ 𝑏 ∈ 2o)) → (𝑇‘(𝑎𝑀𝑏)) = (𝑇‘〈𝑎, (1o ∖ 𝑏)〉)) |
6 | | df-ov 7275 |
. . . . . . 7
⊢ (𝑎𝑇(1o ∖ 𝑏)) = (𝑇‘〈𝑎, (1o ∖ 𝑏)〉) |
7 | 5, 6 | eqtr4di 2798 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑎 ∈ 𝐼 ∧ 𝑏 ∈ 2o)) → (𝑇‘(𝑎𝑀𝑏)) = (𝑎𝑇(1o ∖ 𝑏))) |
8 | | elpri 4589 |
. . . . . . . . 9
⊢ (𝑏 ∈ {∅, 1o}
→ (𝑏 = ∅ ∨
𝑏 =
1o)) |
9 | | df2o3 8297 |
. . . . . . . . 9
⊢
2o = {∅, 1o} |
10 | 8, 9 | eleq2s 2859 |
. . . . . . . 8
⊢ (𝑏 ∈ 2o →
(𝑏 = ∅ ∨ 𝑏 =
1o)) |
11 | | simpr 485 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑎 ∈ 𝐼) → 𝑎 ∈ 𝐼) |
12 | | 1oex 8299 |
. . . . . . . . . . . . . 14
⊢
1o ∈ V |
13 | 12 | prid2 4705 |
. . . . . . . . . . . . 13
⊢
1o ∈ {∅, 1o} |
14 | 13, 9 | eleqtrri 2840 |
. . . . . . . . . . . 12
⊢
1o ∈ 2o |
15 | | 1n0 8310 |
. . . . . . . . . . . . . . . 16
⊢
1o ≠ ∅ |
16 | | neeq1 3008 |
. . . . . . . . . . . . . . . 16
⊢ (𝑧 = 1o → (𝑧 ≠ ∅ ↔
1o ≠ ∅)) |
17 | 15, 16 | mpbiri 257 |
. . . . . . . . . . . . . . 15
⊢ (𝑧 = 1o → 𝑧 ≠ ∅) |
18 | | ifnefalse 4477 |
. . . . . . . . . . . . . . 15
⊢ (𝑧 ≠ ∅ → if(𝑧 = ∅, (𝐹‘𝑦), (𝑁‘(𝐹‘𝑦))) = (𝑁‘(𝐹‘𝑦))) |
19 | 17, 18 | syl 17 |
. . . . . . . . . . . . . 14
⊢ (𝑧 = 1o → if(𝑧 = ∅, (𝐹‘𝑦), (𝑁‘(𝐹‘𝑦))) = (𝑁‘(𝐹‘𝑦))) |
20 | | fveq2 6771 |
. . . . . . . . . . . . . . 15
⊢ (𝑦 = 𝑎 → (𝐹‘𝑦) = (𝐹‘𝑎)) |
21 | 20 | fveq2d 6775 |
. . . . . . . . . . . . . 14
⊢ (𝑦 = 𝑎 → (𝑁‘(𝐹‘𝑦)) = (𝑁‘(𝐹‘𝑎))) |
22 | 19, 21 | sylan9eqr 2802 |
. . . . . . . . . . . . 13
⊢ ((𝑦 = 𝑎 ∧ 𝑧 = 1o) → if(𝑧 = ∅, (𝐹‘𝑦), (𝑁‘(𝐹‘𝑦))) = (𝑁‘(𝐹‘𝑎))) |
23 | | frgpup.t |
. . . . . . . . . . . . 13
⊢ 𝑇 = (𝑦 ∈ 𝐼, 𝑧 ∈ 2o ↦ if(𝑧 = ∅, (𝐹‘𝑦), (𝑁‘(𝐹‘𝑦)))) |
24 | | fvex 6784 |
. . . . . . . . . . . . 13
⊢ (𝑁‘(𝐹‘𝑎)) ∈ V |
25 | 22, 23, 24 | ovmpoa 7423 |
. . . . . . . . . . . 12
⊢ ((𝑎 ∈ 𝐼 ∧ 1o ∈ 2o)
→ (𝑎𝑇1o) = (𝑁‘(𝐹‘𝑎))) |
26 | 11, 14, 25 | sylancl 586 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑎 ∈ 𝐼) → (𝑎𝑇1o) = (𝑁‘(𝐹‘𝑎))) |
27 | | 0ex 5235 |
. . . . . . . . . . . . . . 15
⊢ ∅
∈ V |
28 | 27 | prid1 4704 |
. . . . . . . . . . . . . 14
⊢ ∅
∈ {∅, 1o} |
29 | 28, 9 | eleqtrri 2840 |
. . . . . . . . . . . . 13
⊢ ∅
∈ 2o |
30 | | iftrue 4471 |
. . . . . . . . . . . . . . 15
⊢ (𝑧 = ∅ → if(𝑧 = ∅, (𝐹‘𝑦), (𝑁‘(𝐹‘𝑦))) = (𝐹‘𝑦)) |
31 | 30, 20 | sylan9eqr 2802 |
. . . . . . . . . . . . . 14
⊢ ((𝑦 = 𝑎 ∧ 𝑧 = ∅) → if(𝑧 = ∅, (𝐹‘𝑦), (𝑁‘(𝐹‘𝑦))) = (𝐹‘𝑎)) |
32 | | fvex 6784 |
. . . . . . . . . . . . . 14
⊢ (𝐹‘𝑎) ∈ V |
33 | 31, 23, 32 | ovmpoa 7423 |
. . . . . . . . . . . . 13
⊢ ((𝑎 ∈ 𝐼 ∧ ∅ ∈ 2o) →
(𝑎𝑇∅) = (𝐹‘𝑎)) |
34 | 11, 29, 33 | sylancl 586 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑎 ∈ 𝐼) → (𝑎𝑇∅) = (𝐹‘𝑎)) |
35 | 34 | fveq2d 6775 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑎 ∈ 𝐼) → (𝑁‘(𝑎𝑇∅)) = (𝑁‘(𝐹‘𝑎))) |
36 | 26, 35 | eqtr4d 2783 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑎 ∈ 𝐼) → (𝑎𝑇1o) = (𝑁‘(𝑎𝑇∅))) |
37 | | difeq2 4056 |
. . . . . . . . . . . . 13
⊢ (𝑏 = ∅ → (1o
∖ 𝑏) = (1o
∖ ∅)) |
38 | | dif0 4312 |
. . . . . . . . . . . . 13
⊢
(1o ∖ ∅) = 1o |
39 | 37, 38 | eqtrdi 2796 |
. . . . . . . . . . . 12
⊢ (𝑏 = ∅ → (1o
∖ 𝑏) =
1o) |
40 | 39 | oveq2d 7288 |
. . . . . . . . . . 11
⊢ (𝑏 = ∅ → (𝑎𝑇(1o ∖ 𝑏)) = (𝑎𝑇1o)) |
41 | | oveq2 7280 |
. . . . . . . . . . . 12
⊢ (𝑏 = ∅ → (𝑎𝑇𝑏) = (𝑎𝑇∅)) |
42 | 41 | fveq2d 6775 |
. . . . . . . . . . 11
⊢ (𝑏 = ∅ → (𝑁‘(𝑎𝑇𝑏)) = (𝑁‘(𝑎𝑇∅))) |
43 | 40, 42 | eqeq12d 2756 |
. . . . . . . . . 10
⊢ (𝑏 = ∅ → ((𝑎𝑇(1o ∖ 𝑏)) = (𝑁‘(𝑎𝑇𝑏)) ↔ (𝑎𝑇1o) = (𝑁‘(𝑎𝑇∅)))) |
44 | 36, 43 | syl5ibrcom 246 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑎 ∈ 𝐼) → (𝑏 = ∅ → (𝑎𝑇(1o ∖ 𝑏)) = (𝑁‘(𝑎𝑇𝑏)))) |
45 | 36 | fveq2d 6775 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑎 ∈ 𝐼) → (𝑁‘(𝑎𝑇1o)) = (𝑁‘(𝑁‘(𝑎𝑇∅)))) |
46 | | frgpup.h |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝐻 ∈ Grp) |
47 | | frgpup.a |
. . . . . . . . . . . . . 14
⊢ (𝜑 → 𝐹:𝐼⟶𝐵) |
48 | 47 | ffvelrnda 6958 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑎 ∈ 𝐼) → (𝐹‘𝑎) ∈ 𝐵) |
49 | 34, 48 | eqeltrd 2841 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑎 ∈ 𝐼) → (𝑎𝑇∅) ∈ 𝐵) |
50 | | frgpup.b |
. . . . . . . . . . . . 13
⊢ 𝐵 = (Base‘𝐻) |
51 | | frgpup.n |
. . . . . . . . . . . . 13
⊢ 𝑁 = (invg‘𝐻) |
52 | 50, 51 | grpinvinv 18653 |
. . . . . . . . . . . 12
⊢ ((𝐻 ∈ Grp ∧ (𝑎𝑇∅) ∈ 𝐵) → (𝑁‘(𝑁‘(𝑎𝑇∅))) = (𝑎𝑇∅)) |
53 | 46, 49, 52 | syl2an2r 682 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑎 ∈ 𝐼) → (𝑁‘(𝑁‘(𝑎𝑇∅))) = (𝑎𝑇∅)) |
54 | 45, 53 | eqtr2d 2781 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑎 ∈ 𝐼) → (𝑎𝑇∅) = (𝑁‘(𝑎𝑇1o))) |
55 | | difeq2 4056 |
. . . . . . . . . . . . 13
⊢ (𝑏 = 1o →
(1o ∖ 𝑏) =
(1o ∖ 1o)) |
56 | | difid 4310 |
. . . . . . . . . . . . 13
⊢
(1o ∖ 1o) = ∅ |
57 | 55, 56 | eqtrdi 2796 |
. . . . . . . . . . . 12
⊢ (𝑏 = 1o →
(1o ∖ 𝑏) =
∅) |
58 | 57 | oveq2d 7288 |
. . . . . . . . . . 11
⊢ (𝑏 = 1o → (𝑎𝑇(1o ∖ 𝑏)) = (𝑎𝑇∅)) |
59 | | oveq2 7280 |
. . . . . . . . . . . 12
⊢ (𝑏 = 1o → (𝑎𝑇𝑏) = (𝑎𝑇1o)) |
60 | 59 | fveq2d 6775 |
. . . . . . . . . . 11
⊢ (𝑏 = 1o → (𝑁‘(𝑎𝑇𝑏)) = (𝑁‘(𝑎𝑇1o))) |
61 | 58, 60 | eqeq12d 2756 |
. . . . . . . . . 10
⊢ (𝑏 = 1o → ((𝑎𝑇(1o ∖ 𝑏)) = (𝑁‘(𝑎𝑇𝑏)) ↔ (𝑎𝑇∅) = (𝑁‘(𝑎𝑇1o)))) |
62 | 54, 61 | syl5ibrcom 246 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑎 ∈ 𝐼) → (𝑏 = 1o → (𝑎𝑇(1o ∖ 𝑏)) = (𝑁‘(𝑎𝑇𝑏)))) |
63 | 44, 62 | jaod 856 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑎 ∈ 𝐼) → ((𝑏 = ∅ ∨ 𝑏 = 1o) → (𝑎𝑇(1o ∖ 𝑏)) = (𝑁‘(𝑎𝑇𝑏)))) |
64 | 10, 63 | syl5 34 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑎 ∈ 𝐼) → (𝑏 ∈ 2o → (𝑎𝑇(1o ∖ 𝑏)) = (𝑁‘(𝑎𝑇𝑏)))) |
65 | 64 | impr 455 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑎 ∈ 𝐼 ∧ 𝑏 ∈ 2o)) → (𝑎𝑇(1o ∖ 𝑏)) = (𝑁‘(𝑎𝑇𝑏))) |
66 | 7, 65 | eqtrd 2780 |
. . . . 5
⊢ ((𝜑 ∧ (𝑎 ∈ 𝐼 ∧ 𝑏 ∈ 2o)) → (𝑇‘(𝑎𝑀𝑏)) = (𝑁‘(𝑎𝑇𝑏))) |
67 | | fveq2 6771 |
. . . . . . . 8
⊢ (𝐴 = 〈𝑎, 𝑏〉 → (𝑀‘𝐴) = (𝑀‘〈𝑎, 𝑏〉)) |
68 | | df-ov 7275 |
. . . . . . . 8
⊢ (𝑎𝑀𝑏) = (𝑀‘〈𝑎, 𝑏〉) |
69 | 67, 68 | eqtr4di 2798 |
. . . . . . 7
⊢ (𝐴 = 〈𝑎, 𝑏〉 → (𝑀‘𝐴) = (𝑎𝑀𝑏)) |
70 | 69 | fveq2d 6775 |
. . . . . 6
⊢ (𝐴 = 〈𝑎, 𝑏〉 → (𝑇‘(𝑀‘𝐴)) = (𝑇‘(𝑎𝑀𝑏))) |
71 | | fveq2 6771 |
. . . . . . . 8
⊢ (𝐴 = 〈𝑎, 𝑏〉 → (𝑇‘𝐴) = (𝑇‘〈𝑎, 𝑏〉)) |
72 | | df-ov 7275 |
. . . . . . . 8
⊢ (𝑎𝑇𝑏) = (𝑇‘〈𝑎, 𝑏〉) |
73 | 71, 72 | eqtr4di 2798 |
. . . . . . 7
⊢ (𝐴 = 〈𝑎, 𝑏〉 → (𝑇‘𝐴) = (𝑎𝑇𝑏)) |
74 | 73 | fveq2d 6775 |
. . . . . 6
⊢ (𝐴 = 〈𝑎, 𝑏〉 → (𝑁‘(𝑇‘𝐴)) = (𝑁‘(𝑎𝑇𝑏))) |
75 | 70, 74 | eqeq12d 2756 |
. . . . 5
⊢ (𝐴 = 〈𝑎, 𝑏〉 → ((𝑇‘(𝑀‘𝐴)) = (𝑁‘(𝑇‘𝐴)) ↔ (𝑇‘(𝑎𝑀𝑏)) = (𝑁‘(𝑎𝑇𝑏)))) |
76 | 66, 75 | syl5ibrcom 246 |
. . . 4
⊢ ((𝜑 ∧ (𝑎 ∈ 𝐼 ∧ 𝑏 ∈ 2o)) → (𝐴 = 〈𝑎, 𝑏〉 → (𝑇‘(𝑀‘𝐴)) = (𝑁‘(𝑇‘𝐴)))) |
77 | 76 | rexlimdvva 3225 |
. . 3
⊢ (𝜑 → (∃𝑎 ∈ 𝐼 ∃𝑏 ∈ 2o 𝐴 = 〈𝑎, 𝑏〉 → (𝑇‘(𝑀‘𝐴)) = (𝑁‘(𝑇‘𝐴)))) |
78 | 1, 77 | syl5bi 241 |
. 2
⊢ (𝜑 → (𝐴 ∈ (𝐼 × 2o) → (𝑇‘(𝑀‘𝐴)) = (𝑁‘(𝑇‘𝐴)))) |
79 | 78 | imp 407 |
1
⊢ ((𝜑 ∧ 𝐴 ∈ (𝐼 × 2o)) → (𝑇‘(𝑀‘𝐴)) = (𝑁‘(𝑇‘𝐴))) |