Step | Hyp | Ref
| Expression |
1 | | elxp2 5056 |
. . 3
⊢ (𝐴 ∈ (𝐼 × 2𝑜) ↔
∃𝑎 ∈ 𝐼 ∃𝑏 ∈ 2𝑜 𝐴 = 〈𝑎, 𝑏〉) |
2 | | frgpuptinv.m |
. . . . . . . . . 10
⊢ 𝑀 = (𝑦 ∈ 𝐼, 𝑧 ∈ 2𝑜 ↦
〈𝑦,
(1𝑜 ∖ 𝑧)〉) |
3 | 2 | efgmval 17948 |
. . . . . . . . 9
⊢ ((𝑎 ∈ 𝐼 ∧ 𝑏 ∈ 2𝑜) → (𝑎𝑀𝑏) = 〈𝑎, (1𝑜 ∖ 𝑏)〉) |
4 | 3 | adantl 481 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑎 ∈ 𝐼 ∧ 𝑏 ∈ 2𝑜)) → (𝑎𝑀𝑏) = 〈𝑎, (1𝑜 ∖ 𝑏)〉) |
5 | 4 | fveq2d 6107 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑎 ∈ 𝐼 ∧ 𝑏 ∈ 2𝑜)) → (𝑇‘(𝑎𝑀𝑏)) = (𝑇‘〈𝑎, (1𝑜 ∖ 𝑏)〉)) |
6 | | df-ov 6552 |
. . . . . . 7
⊢ (𝑎𝑇(1𝑜 ∖ 𝑏)) = (𝑇‘〈𝑎, (1𝑜 ∖ 𝑏)〉) |
7 | 5, 6 | syl6eqr 2662 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑎 ∈ 𝐼 ∧ 𝑏 ∈ 2𝑜)) → (𝑇‘(𝑎𝑀𝑏)) = (𝑎𝑇(1𝑜 ∖ 𝑏))) |
8 | | elpri 4145 |
. . . . . . . . 9
⊢ (𝑏 ∈ {∅,
1𝑜} → (𝑏 = ∅ ∨ 𝑏 = 1𝑜)) |
9 | | df2o3 7460 |
. . . . . . . . 9
⊢
2𝑜 = {∅,
1𝑜} |
10 | 8, 9 | eleq2s 2706 |
. . . . . . . 8
⊢ (𝑏 ∈ 2𝑜
→ (𝑏 = ∅ ∨
𝑏 =
1𝑜)) |
11 | | simpr 476 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑎 ∈ 𝐼) → 𝑎 ∈ 𝐼) |
12 | | 1on 7454 |
. . . . . . . . . . . . . . 15
⊢
1𝑜 ∈ On |
13 | 12 | elexi 3186 |
. . . . . . . . . . . . . 14
⊢
1𝑜 ∈ V |
14 | 13 | prid2 4242 |
. . . . . . . . . . . . 13
⊢
1𝑜 ∈ {∅,
1𝑜} |
15 | 14, 9 | eleqtrri 2687 |
. . . . . . . . . . . 12
⊢
1𝑜 ∈ 2𝑜 |
16 | | 1n0 7462 |
. . . . . . . . . . . . . . . 16
⊢
1𝑜 ≠ ∅ |
17 | | neeq1 2844 |
. . . . . . . . . . . . . . . 16
⊢ (𝑧 = 1𝑜 →
(𝑧 ≠ ∅ ↔
1𝑜 ≠ ∅)) |
18 | 16, 17 | mpbiri 247 |
. . . . . . . . . . . . . . 15
⊢ (𝑧 = 1𝑜 →
𝑧 ≠
∅) |
19 | | ifnefalse 4048 |
. . . . . . . . . . . . . . 15
⊢ (𝑧 ≠ ∅ → if(𝑧 = ∅, (𝐹‘𝑦), (𝑁‘(𝐹‘𝑦))) = (𝑁‘(𝐹‘𝑦))) |
20 | 18, 19 | syl 17 |
. . . . . . . . . . . . . 14
⊢ (𝑧 = 1𝑜 →
if(𝑧 = ∅, (𝐹‘𝑦), (𝑁‘(𝐹‘𝑦))) = (𝑁‘(𝐹‘𝑦))) |
21 | | fveq2 6103 |
. . . . . . . . . . . . . . 15
⊢ (𝑦 = 𝑎 → (𝐹‘𝑦) = (𝐹‘𝑎)) |
22 | 21 | fveq2d 6107 |
. . . . . . . . . . . . . 14
⊢ (𝑦 = 𝑎 → (𝑁‘(𝐹‘𝑦)) = (𝑁‘(𝐹‘𝑎))) |
23 | 20, 22 | sylan9eqr 2666 |
. . . . . . . . . . . . 13
⊢ ((𝑦 = 𝑎 ∧ 𝑧 = 1𝑜) → if(𝑧 = ∅, (𝐹‘𝑦), (𝑁‘(𝐹‘𝑦))) = (𝑁‘(𝐹‘𝑎))) |
24 | | frgpup.t |
. . . . . . . . . . . . 13
⊢ 𝑇 = (𝑦 ∈ 𝐼, 𝑧 ∈ 2𝑜 ↦
if(𝑧 = ∅, (𝐹‘𝑦), (𝑁‘(𝐹‘𝑦)))) |
25 | | fvex 6113 |
. . . . . . . . . . . . 13
⊢ (𝑁‘(𝐹‘𝑎)) ∈ V |
26 | 23, 24, 25 | ovmpt2a 6689 |
. . . . . . . . . . . 12
⊢ ((𝑎 ∈ 𝐼 ∧ 1𝑜 ∈
2𝑜) → (𝑎𝑇1𝑜) = (𝑁‘(𝐹‘𝑎))) |
27 | 11, 15, 26 | sylancl 693 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑎 ∈ 𝐼) → (𝑎𝑇1𝑜) = (𝑁‘(𝐹‘𝑎))) |
28 | | 0ex 4718 |
. . . . . . . . . . . . . . 15
⊢ ∅
∈ V |
29 | 28 | prid1 4241 |
. . . . . . . . . . . . . 14
⊢ ∅
∈ {∅, 1𝑜} |
30 | 29, 9 | eleqtrri 2687 |
. . . . . . . . . . . . 13
⊢ ∅
∈ 2𝑜 |
31 | | iftrue 4042 |
. . . . . . . . . . . . . . 15
⊢ (𝑧 = ∅ → if(𝑧 = ∅, (𝐹‘𝑦), (𝑁‘(𝐹‘𝑦))) = (𝐹‘𝑦)) |
32 | 31, 21 | sylan9eqr 2666 |
. . . . . . . . . . . . . 14
⊢ ((𝑦 = 𝑎 ∧ 𝑧 = ∅) → if(𝑧 = ∅, (𝐹‘𝑦), (𝑁‘(𝐹‘𝑦))) = (𝐹‘𝑎)) |
33 | | fvex 6113 |
. . . . . . . . . . . . . 14
⊢ (𝐹‘𝑎) ∈ V |
34 | 32, 24, 33 | ovmpt2a 6689 |
. . . . . . . . . . . . 13
⊢ ((𝑎 ∈ 𝐼 ∧ ∅ ∈ 2𝑜)
→ (𝑎𝑇∅) = (𝐹‘𝑎)) |
35 | 11, 30, 34 | sylancl 693 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑎 ∈ 𝐼) → (𝑎𝑇∅) = (𝐹‘𝑎)) |
36 | 35 | fveq2d 6107 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑎 ∈ 𝐼) → (𝑁‘(𝑎𝑇∅)) = (𝑁‘(𝐹‘𝑎))) |
37 | 27, 36 | eqtr4d 2647 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑎 ∈ 𝐼) → (𝑎𝑇1𝑜) = (𝑁‘(𝑎𝑇∅))) |
38 | | difeq2 3684 |
. . . . . . . . . . . . 13
⊢ (𝑏 = ∅ →
(1𝑜 ∖ 𝑏) = (1𝑜 ∖
∅)) |
39 | | dif0 3904 |
. . . . . . . . . . . . 13
⊢
(1𝑜 ∖ ∅) =
1𝑜 |
40 | 38, 39 | syl6eq 2660 |
. . . . . . . . . . . 12
⊢ (𝑏 = ∅ →
(1𝑜 ∖ 𝑏) = 1𝑜) |
41 | 40 | oveq2d 6565 |
. . . . . . . . . . 11
⊢ (𝑏 = ∅ → (𝑎𝑇(1𝑜 ∖ 𝑏)) = (𝑎𝑇1𝑜)) |
42 | | oveq2 6557 |
. . . . . . . . . . . 12
⊢ (𝑏 = ∅ → (𝑎𝑇𝑏) = (𝑎𝑇∅)) |
43 | 42 | fveq2d 6107 |
. . . . . . . . . . 11
⊢ (𝑏 = ∅ → (𝑁‘(𝑎𝑇𝑏)) = (𝑁‘(𝑎𝑇∅))) |
44 | 41, 43 | eqeq12d 2625 |
. . . . . . . . . 10
⊢ (𝑏 = ∅ → ((𝑎𝑇(1𝑜 ∖ 𝑏)) = (𝑁‘(𝑎𝑇𝑏)) ↔ (𝑎𝑇1𝑜) = (𝑁‘(𝑎𝑇∅)))) |
45 | 37, 44 | syl5ibrcom 236 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑎 ∈ 𝐼) → (𝑏 = ∅ → (𝑎𝑇(1𝑜 ∖ 𝑏)) = (𝑁‘(𝑎𝑇𝑏)))) |
46 | 37 | fveq2d 6107 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑎 ∈ 𝐼) → (𝑁‘(𝑎𝑇1𝑜)) = (𝑁‘(𝑁‘(𝑎𝑇∅)))) |
47 | | frgpup.h |
. . . . . . . . . . . . 13
⊢ (𝜑 → 𝐻 ∈ Grp) |
48 | 47 | adantr 480 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑎 ∈ 𝐼) → 𝐻 ∈ Grp) |
49 | | frgpup.a |
. . . . . . . . . . . . . 14
⊢ (𝜑 → 𝐹:𝐼⟶𝐵) |
50 | 49 | ffvelrnda 6267 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑎 ∈ 𝐼) → (𝐹‘𝑎) ∈ 𝐵) |
51 | 35, 50 | eqeltrd 2688 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑎 ∈ 𝐼) → (𝑎𝑇∅) ∈ 𝐵) |
52 | | frgpup.b |
. . . . . . . . . . . . 13
⊢ 𝐵 = (Base‘𝐻) |
53 | | frgpup.n |
. . . . . . . . . . . . 13
⊢ 𝑁 = (invg‘𝐻) |
54 | 52, 53 | grpinvinv 17305 |
. . . . . . . . . . . 12
⊢ ((𝐻 ∈ Grp ∧ (𝑎𝑇∅) ∈ 𝐵) → (𝑁‘(𝑁‘(𝑎𝑇∅))) = (𝑎𝑇∅)) |
55 | 48, 51, 54 | syl2anc 691 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑎 ∈ 𝐼) → (𝑁‘(𝑁‘(𝑎𝑇∅))) = (𝑎𝑇∅)) |
56 | 46, 55 | eqtr2d 2645 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑎 ∈ 𝐼) → (𝑎𝑇∅) = (𝑁‘(𝑎𝑇1𝑜))) |
57 | | difeq2 3684 |
. . . . . . . . . . . . 13
⊢ (𝑏 = 1𝑜 →
(1𝑜 ∖ 𝑏) = (1𝑜 ∖
1𝑜)) |
58 | | difid 3902 |
. . . . . . . . . . . . 13
⊢
(1𝑜 ∖ 1𝑜) =
∅ |
59 | 57, 58 | syl6eq 2660 |
. . . . . . . . . . . 12
⊢ (𝑏 = 1𝑜 →
(1𝑜 ∖ 𝑏) = ∅) |
60 | 59 | oveq2d 6565 |
. . . . . . . . . . 11
⊢ (𝑏 = 1𝑜 →
(𝑎𝑇(1𝑜 ∖ 𝑏)) = (𝑎𝑇∅)) |
61 | | oveq2 6557 |
. . . . . . . . . . . 12
⊢ (𝑏 = 1𝑜 →
(𝑎𝑇𝑏) = (𝑎𝑇1𝑜)) |
62 | 61 | fveq2d 6107 |
. . . . . . . . . . 11
⊢ (𝑏 = 1𝑜 →
(𝑁‘(𝑎𝑇𝑏)) = (𝑁‘(𝑎𝑇1𝑜))) |
63 | 60, 62 | eqeq12d 2625 |
. . . . . . . . . 10
⊢ (𝑏 = 1𝑜 →
((𝑎𝑇(1𝑜 ∖ 𝑏)) = (𝑁‘(𝑎𝑇𝑏)) ↔ (𝑎𝑇∅) = (𝑁‘(𝑎𝑇1𝑜)))) |
64 | 56, 63 | syl5ibrcom 236 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑎 ∈ 𝐼) → (𝑏 = 1𝑜 → (𝑎𝑇(1𝑜 ∖ 𝑏)) = (𝑁‘(𝑎𝑇𝑏)))) |
65 | 45, 64 | jaod 394 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑎 ∈ 𝐼) → ((𝑏 = ∅ ∨ 𝑏 = 1𝑜) → (𝑎𝑇(1𝑜 ∖ 𝑏)) = (𝑁‘(𝑎𝑇𝑏)))) |
66 | 10, 65 | syl5 33 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑎 ∈ 𝐼) → (𝑏 ∈ 2𝑜 → (𝑎𝑇(1𝑜 ∖ 𝑏)) = (𝑁‘(𝑎𝑇𝑏)))) |
67 | 66 | impr 647 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑎 ∈ 𝐼 ∧ 𝑏 ∈ 2𝑜)) → (𝑎𝑇(1𝑜 ∖ 𝑏)) = (𝑁‘(𝑎𝑇𝑏))) |
68 | 7, 67 | eqtrd 2644 |
. . . . 5
⊢ ((𝜑 ∧ (𝑎 ∈ 𝐼 ∧ 𝑏 ∈ 2𝑜)) → (𝑇‘(𝑎𝑀𝑏)) = (𝑁‘(𝑎𝑇𝑏))) |
69 | | fveq2 6103 |
. . . . . . . 8
⊢ (𝐴 = 〈𝑎, 𝑏〉 → (𝑀‘𝐴) = (𝑀‘〈𝑎, 𝑏〉)) |
70 | | df-ov 6552 |
. . . . . . . 8
⊢ (𝑎𝑀𝑏) = (𝑀‘〈𝑎, 𝑏〉) |
71 | 69, 70 | syl6eqr 2662 |
. . . . . . 7
⊢ (𝐴 = 〈𝑎, 𝑏〉 → (𝑀‘𝐴) = (𝑎𝑀𝑏)) |
72 | 71 | fveq2d 6107 |
. . . . . 6
⊢ (𝐴 = 〈𝑎, 𝑏〉 → (𝑇‘(𝑀‘𝐴)) = (𝑇‘(𝑎𝑀𝑏))) |
73 | | fveq2 6103 |
. . . . . . . 8
⊢ (𝐴 = 〈𝑎, 𝑏〉 → (𝑇‘𝐴) = (𝑇‘〈𝑎, 𝑏〉)) |
74 | | df-ov 6552 |
. . . . . . . 8
⊢ (𝑎𝑇𝑏) = (𝑇‘〈𝑎, 𝑏〉) |
75 | 73, 74 | syl6eqr 2662 |
. . . . . . 7
⊢ (𝐴 = 〈𝑎, 𝑏〉 → (𝑇‘𝐴) = (𝑎𝑇𝑏)) |
76 | 75 | fveq2d 6107 |
. . . . . 6
⊢ (𝐴 = 〈𝑎, 𝑏〉 → (𝑁‘(𝑇‘𝐴)) = (𝑁‘(𝑎𝑇𝑏))) |
77 | 72, 76 | eqeq12d 2625 |
. . . . 5
⊢ (𝐴 = 〈𝑎, 𝑏〉 → ((𝑇‘(𝑀‘𝐴)) = (𝑁‘(𝑇‘𝐴)) ↔ (𝑇‘(𝑎𝑀𝑏)) = (𝑁‘(𝑎𝑇𝑏)))) |
78 | 68, 77 | syl5ibrcom 236 |
. . . 4
⊢ ((𝜑 ∧ (𝑎 ∈ 𝐼 ∧ 𝑏 ∈ 2𝑜)) → (𝐴 = 〈𝑎, 𝑏〉 → (𝑇‘(𝑀‘𝐴)) = (𝑁‘(𝑇‘𝐴)))) |
79 | 78 | rexlimdvva 3020 |
. . 3
⊢ (𝜑 → (∃𝑎 ∈ 𝐼 ∃𝑏 ∈ 2𝑜 𝐴 = 〈𝑎, 𝑏〉 → (𝑇‘(𝑀‘𝐴)) = (𝑁‘(𝑇‘𝐴)))) |
80 | 1, 79 | syl5bi 231 |
. 2
⊢ (𝜑 → (𝐴 ∈ (𝐼 × 2𝑜) →
(𝑇‘(𝑀‘𝐴)) = (𝑁‘(𝑇‘𝐴)))) |
81 | 80 | imp 444 |
1
⊢ ((𝜑 ∧ 𝐴 ∈ (𝐼 × 2𝑜)) →
(𝑇‘(𝑀‘𝐴)) = (𝑁‘(𝑇‘𝐴))) |