| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | eqid 2736 | . 2
⊢
(Cntz‘𝐺) =
(Cntz‘𝐺) | 
| 2 |  | eqid 2736 | . 2
⊢
(0g‘𝐺) = (0g‘𝐺) | 
| 3 |  | dprd2d.k | . 2
⊢ 𝐾 =
(mrCls‘(SubGrp‘𝐺)) | 
| 4 |  | dprd2d.5 | . . 3
⊢ (𝜑 → 𝐺dom DProd (𝑖 ∈ 𝐼 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗))))) | 
| 5 |  | dprdgrp 20026 | . . 3
⊢ (𝐺dom DProd (𝑖 ∈ 𝐼 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗)))) → 𝐺 ∈ Grp) | 
| 6 | 4, 5 | syl 17 | . 2
⊢ (𝜑 → 𝐺 ∈ Grp) | 
| 7 |  | resiun2 6017 | . . . . 5
⊢ (𝐴 ↾ ∪ 𝑖 ∈ 𝐼 {𝑖}) = ∪
𝑖 ∈ 𝐼 (𝐴 ↾ {𝑖}) | 
| 8 |  | iunid 5059 | . . . . . 6
⊢ ∪ 𝑖 ∈ 𝐼 {𝑖} = 𝐼 | 
| 9 | 8 | reseq2i 5993 | . . . . 5
⊢ (𝐴 ↾ ∪ 𝑖 ∈ 𝐼 {𝑖}) = (𝐴 ↾ 𝐼) | 
| 10 | 7, 9 | eqtr3i 2766 | . . . 4
⊢ ∪ 𝑖 ∈ 𝐼 (𝐴 ↾ {𝑖}) = (𝐴 ↾ 𝐼) | 
| 11 |  | dprd2d.1 | . . . . 5
⊢ (𝜑 → Rel 𝐴) | 
| 12 |  | dprd2d.3 | . . . . 5
⊢ (𝜑 → dom 𝐴 ⊆ 𝐼) | 
| 13 |  | relssres 6039 | . . . . 5
⊢ ((Rel
𝐴 ∧ dom 𝐴 ⊆ 𝐼) → (𝐴 ↾ 𝐼) = 𝐴) | 
| 14 | 11, 12, 13 | syl2anc 584 | . . . 4
⊢ (𝜑 → (𝐴 ↾ 𝐼) = 𝐴) | 
| 15 | 10, 14 | eqtrid 2788 | . . 3
⊢ (𝜑 → ∪ 𝑖 ∈ 𝐼 (𝐴 ↾ {𝑖}) = 𝐴) | 
| 16 |  | ovex 7465 | . . . . . 6
⊢ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗))) ∈ V | 
| 17 |  | eqid 2736 | . . . . . 6
⊢ (𝑖 ∈ 𝐼 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗)))) = (𝑖 ∈ 𝐼 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗)))) | 
| 18 | 16, 17 | dmmpti 6711 | . . . . 5
⊢ dom
(𝑖 ∈ 𝐼 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗)))) = 𝐼 | 
| 19 |  | reldmdprd 20018 | . . . . . . 7
⊢ Rel dom
DProd | 
| 20 | 19 | brrelex2i 5741 | . . . . . 6
⊢ (𝐺dom DProd (𝑖 ∈ 𝐼 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗)))) → (𝑖 ∈ 𝐼 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗)))) ∈ V) | 
| 21 |  | dmexg 7924 | . . . . . 6
⊢ ((𝑖 ∈ 𝐼 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗)))) ∈ V → dom (𝑖 ∈ 𝐼 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗)))) ∈ V) | 
| 22 | 4, 20, 21 | 3syl 18 | . . . . 5
⊢ (𝜑 → dom (𝑖 ∈ 𝐼 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗)))) ∈ V) | 
| 23 | 18, 22 | eqeltrrid 2845 | . . . 4
⊢ (𝜑 → 𝐼 ∈ V) | 
| 24 |  | ressn 6304 | . . . . . 6
⊢ (𝐴 ↾ {𝑖}) = ({𝑖} × (𝐴 “ {𝑖})) | 
| 25 |  | vsnex 5433 | . . . . . . 7
⊢ {𝑖} ∈ V | 
| 26 |  | ovex 7465 | . . . . . . . . 9
⊢ (𝑖𝑆𝑗) ∈ V | 
| 27 |  | eqid 2736 | . . . . . . . . 9
⊢ (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗)) = (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗)) | 
| 28 | 26, 27 | dmmpti 6711 | . . . . . . . 8
⊢ dom
(𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗)) = (𝐴 “ {𝑖}) | 
| 29 |  | dprd2d.4 | . . . . . . . . 9
⊢ ((𝜑 ∧ 𝑖 ∈ 𝐼) → 𝐺dom DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗))) | 
| 30 | 19 | brrelex2i 5741 | . . . . . . . . 9
⊢ (𝐺dom DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗)) → (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗)) ∈ V) | 
| 31 |  | dmexg 7924 | . . . . . . . . 9
⊢ ((𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗)) ∈ V → dom (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗)) ∈ V) | 
| 32 | 29, 30, 31 | 3syl 18 | . . . . . . . 8
⊢ ((𝜑 ∧ 𝑖 ∈ 𝐼) → dom (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗)) ∈ V) | 
| 33 | 28, 32 | eqeltrrid 2845 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑖 ∈ 𝐼) → (𝐴 “ {𝑖}) ∈ V) | 
| 34 |  | xpexg 7771 | . . . . . . 7
⊢ (({𝑖} ∈ V ∧ (𝐴 “ {𝑖}) ∈ V) → ({𝑖} × (𝐴 “ {𝑖})) ∈ V) | 
| 35 | 25, 33, 34 | sylancr 587 | . . . . . 6
⊢ ((𝜑 ∧ 𝑖 ∈ 𝐼) → ({𝑖} × (𝐴 “ {𝑖})) ∈ V) | 
| 36 | 24, 35 | eqeltrid 2844 | . . . . 5
⊢ ((𝜑 ∧ 𝑖 ∈ 𝐼) → (𝐴 ↾ {𝑖}) ∈ V) | 
| 37 | 36 | ralrimiva 3145 | . . . 4
⊢ (𝜑 → ∀𝑖 ∈ 𝐼 (𝐴 ↾ {𝑖}) ∈ V) | 
| 38 |  | iunexg 7989 | . . . 4
⊢ ((𝐼 ∈ V ∧ ∀𝑖 ∈ 𝐼 (𝐴 ↾ {𝑖}) ∈ V) → ∪ 𝑖 ∈ 𝐼 (𝐴 ↾ {𝑖}) ∈ V) | 
| 39 | 23, 37, 38 | syl2anc 584 | . . 3
⊢ (𝜑 → ∪ 𝑖 ∈ 𝐼 (𝐴 ↾ {𝑖}) ∈ V) | 
| 40 | 15, 39 | eqeltrrd 2841 | . 2
⊢ (𝜑 → 𝐴 ∈ V) | 
| 41 |  | dprd2d.2 | . 2
⊢ (𝜑 → 𝑆:𝐴⟶(SubGrp‘𝐺)) | 
| 42 |  | sneq 4635 | . . . . . . . . . . 11
⊢ (𝑖 = (1st ‘𝑥) → {𝑖} = {(1st ‘𝑥)}) | 
| 43 | 42 | imaeq2d 6077 | . . . . . . . . . 10
⊢ (𝑖 = (1st ‘𝑥) → (𝐴 “ {𝑖}) = (𝐴 “ {(1st ‘𝑥)})) | 
| 44 |  | oveq1 7439 | . . . . . . . . . 10
⊢ (𝑖 = (1st ‘𝑥) → (𝑖𝑆𝑗) = ((1st ‘𝑥)𝑆𝑗)) | 
| 45 | 43, 44 | mpteq12dv 5232 | . . . . . . . . 9
⊢ (𝑖 = (1st ‘𝑥) → (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗)) = (𝑗 ∈ (𝐴 “ {(1st ‘𝑥)}) ↦ ((1st
‘𝑥)𝑆𝑗))) | 
| 46 | 45 | breq2d 5154 | . . . . . . . 8
⊢ (𝑖 = (1st ‘𝑥) → (𝐺dom DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗)) ↔ 𝐺dom DProd (𝑗 ∈ (𝐴 “ {(1st ‘𝑥)}) ↦ ((1st
‘𝑥)𝑆𝑗)))) | 
| 47 | 29 | ralrimiva 3145 | . . . . . . . . 9
⊢ (𝜑 → ∀𝑖 ∈ 𝐼 𝐺dom DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗))) | 
| 48 | 47 | adantr 480 | . . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → ∀𝑖 ∈ 𝐼 𝐺dom DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗))) | 
| 49 | 12 | adantr 480 | . . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → dom 𝐴 ⊆ 𝐼) | 
| 50 |  | 1stdm 8066 | . . . . . . . . . 10
⊢ ((Rel
𝐴 ∧ 𝑥 ∈ 𝐴) → (1st ‘𝑥) ∈ dom 𝐴) | 
| 51 | 11, 50 | sylan 580 | . . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (1st ‘𝑥) ∈ dom 𝐴) | 
| 52 | 49, 51 | sseldd 3983 | . . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (1st ‘𝑥) ∈ 𝐼) | 
| 53 | 46, 48, 52 | rspcdva 3622 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐺dom DProd (𝑗 ∈ (𝐴 “ {(1st ‘𝑥)}) ↦ ((1st
‘𝑥)𝑆𝑗))) | 
| 54 | 53 | 3ad2antr1 1188 | . . . . . 6
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ∧ 𝑥 ≠ 𝑦)) → 𝐺dom DProd (𝑗 ∈ (𝐴 “ {(1st ‘𝑥)}) ↦ ((1st
‘𝑥)𝑆𝑗))) | 
| 55 | 54 | adantr 480 | . . . . 5
⊢ (((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ∧ 𝑥 ≠ 𝑦)) ∧ (1st ‘𝑥) = (1st ‘𝑦)) → 𝐺dom DProd (𝑗 ∈ (𝐴 “ {(1st ‘𝑥)}) ↦ ((1st
‘𝑥)𝑆𝑗))) | 
| 56 |  | ovex 7465 | . . . . . . 7
⊢
((1st ‘𝑥)𝑆𝑗) ∈ V | 
| 57 |  | eqid 2736 | . . . . . . 7
⊢ (𝑗 ∈ (𝐴 “ {(1st ‘𝑥)}) ↦ ((1st
‘𝑥)𝑆𝑗)) = (𝑗 ∈ (𝐴 “ {(1st ‘𝑥)}) ↦ ((1st
‘𝑥)𝑆𝑗)) | 
| 58 | 56, 57 | dmmpti 6711 | . . . . . 6
⊢ dom
(𝑗 ∈ (𝐴 “ {(1st
‘𝑥)}) ↦
((1st ‘𝑥)𝑆𝑗)) = (𝐴 “ {(1st ‘𝑥)}) | 
| 59 | 58 | a1i 11 | . . . . 5
⊢ (((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ∧ 𝑥 ≠ 𝑦)) ∧ (1st ‘𝑥) = (1st ‘𝑦)) → dom (𝑗 ∈ (𝐴 “ {(1st ‘𝑥)}) ↦ ((1st
‘𝑥)𝑆𝑗)) = (𝐴 “ {(1st ‘𝑥)})) | 
| 60 |  | 1st2nd 8065 | . . . . . . . . . . 11
⊢ ((Rel
𝐴 ∧ 𝑥 ∈ 𝐴) → 𝑥 = 〈(1st ‘𝑥), (2nd ‘𝑥)〉) | 
| 61 | 11, 60 | sylan 580 | . . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝑥 = 〈(1st ‘𝑥), (2nd ‘𝑥)〉) | 
| 62 |  | simpr 484 | . . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝑥 ∈ 𝐴) | 
| 63 | 61, 62 | eqeltrrd 2841 | . . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 〈(1st ‘𝑥), (2nd ‘𝑥)〉 ∈ 𝐴) | 
| 64 |  | df-br 5143 | . . . . . . . . 9
⊢
((1st ‘𝑥)𝐴(2nd ‘𝑥) ↔ 〈(1st ‘𝑥), (2nd ‘𝑥)〉 ∈ 𝐴) | 
| 65 | 63, 64 | sylibr 234 | . . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (1st ‘𝑥)𝐴(2nd ‘𝑥)) | 
| 66 | 11 | adantr 480 | . . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → Rel 𝐴) | 
| 67 |  | elrelimasn 6103 | . . . . . . . . 9
⊢ (Rel
𝐴 → ((2nd
‘𝑥) ∈ (𝐴 “ {(1st
‘𝑥)}) ↔
(1st ‘𝑥)𝐴(2nd ‘𝑥))) | 
| 68 | 66, 67 | syl 17 | . . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → ((2nd ‘𝑥) ∈ (𝐴 “ {(1st ‘𝑥)}) ↔ (1st
‘𝑥)𝐴(2nd ‘𝑥))) | 
| 69 | 65, 68 | mpbird 257 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (2nd ‘𝑥) ∈ (𝐴 “ {(1st ‘𝑥)})) | 
| 70 | 69 | 3ad2antr1 1188 | . . . . . 6
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ∧ 𝑥 ≠ 𝑦)) → (2nd ‘𝑥) ∈ (𝐴 “ {(1st ‘𝑥)})) | 
| 71 | 70 | adantr 480 | . . . . 5
⊢ (((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ∧ 𝑥 ≠ 𝑦)) ∧ (1st ‘𝑥) = (1st ‘𝑦)) → (2nd
‘𝑥) ∈ (𝐴 “ {(1st
‘𝑥)})) | 
| 72 | 11 | adantr 480 | . . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ∧ 𝑥 ≠ 𝑦)) → Rel 𝐴) | 
| 73 |  | simpr2 1195 | . . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ∧ 𝑥 ≠ 𝑦)) → 𝑦 ∈ 𝐴) | 
| 74 |  | 1st2nd 8065 | . . . . . . . . . . 11
⊢ ((Rel
𝐴 ∧ 𝑦 ∈ 𝐴) → 𝑦 = 〈(1st ‘𝑦), (2nd ‘𝑦)〉) | 
| 75 | 72, 73, 74 | syl2anc 584 | . . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ∧ 𝑥 ≠ 𝑦)) → 𝑦 = 〈(1st ‘𝑦), (2nd ‘𝑦)〉) | 
| 76 | 75, 73 | eqeltrrd 2841 | . . . . . . . . 9
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ∧ 𝑥 ≠ 𝑦)) → 〈(1st ‘𝑦), (2nd ‘𝑦)〉 ∈ 𝐴) | 
| 77 |  | df-br 5143 | . . . . . . . . 9
⊢
((1st ‘𝑦)𝐴(2nd ‘𝑦) ↔ 〈(1st ‘𝑦), (2nd ‘𝑦)〉 ∈ 𝐴) | 
| 78 | 76, 77 | sylibr 234 | . . . . . . . 8
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ∧ 𝑥 ≠ 𝑦)) → (1st ‘𝑦)𝐴(2nd ‘𝑦)) | 
| 79 |  | elrelimasn 6103 | . . . . . . . . 9
⊢ (Rel
𝐴 → ((2nd
‘𝑦) ∈ (𝐴 “ {(1st
‘𝑦)}) ↔
(1st ‘𝑦)𝐴(2nd ‘𝑦))) | 
| 80 | 72, 79 | syl 17 | . . . . . . . 8
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ∧ 𝑥 ≠ 𝑦)) → ((2nd ‘𝑦) ∈ (𝐴 “ {(1st ‘𝑦)}) ↔ (1st
‘𝑦)𝐴(2nd ‘𝑦))) | 
| 81 | 78, 80 | mpbird 257 | . . . . . . 7
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ∧ 𝑥 ≠ 𝑦)) → (2nd ‘𝑦) ∈ (𝐴 “ {(1st ‘𝑦)})) | 
| 82 | 81 | adantr 480 | . . . . . 6
⊢ (((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ∧ 𝑥 ≠ 𝑦)) ∧ (1st ‘𝑥) = (1st ‘𝑦)) → (2nd
‘𝑦) ∈ (𝐴 “ {(1st
‘𝑦)})) | 
| 83 |  | simpr 484 | . . . . . . . 8
⊢ (((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ∧ 𝑥 ≠ 𝑦)) ∧ (1st ‘𝑥) = (1st ‘𝑦)) → (1st
‘𝑥) = (1st
‘𝑦)) | 
| 84 | 83 | sneqd 4637 | . . . . . . 7
⊢ (((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ∧ 𝑥 ≠ 𝑦)) ∧ (1st ‘𝑥) = (1st ‘𝑦)) → {(1st
‘𝑥)} =
{(1st ‘𝑦)}) | 
| 85 | 84 | imaeq2d 6077 | . . . . . 6
⊢ (((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ∧ 𝑥 ≠ 𝑦)) ∧ (1st ‘𝑥) = (1st ‘𝑦)) → (𝐴 “ {(1st ‘𝑥)}) = (𝐴 “ {(1st ‘𝑦)})) | 
| 86 | 82, 85 | eleqtrrd 2843 | . . . . 5
⊢ (((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ∧ 𝑥 ≠ 𝑦)) ∧ (1st ‘𝑥) = (1st ‘𝑦)) → (2nd
‘𝑦) ∈ (𝐴 “ {(1st
‘𝑥)})) | 
| 87 |  | simplr3 1217 | . . . . . 6
⊢ (((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ∧ 𝑥 ≠ 𝑦)) ∧ (1st ‘𝑥) = (1st ‘𝑦)) → 𝑥 ≠ 𝑦) | 
| 88 |  | simpr1 1194 | . . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ∧ 𝑥 ≠ 𝑦)) → 𝑥 ∈ 𝐴) | 
| 89 | 72, 88, 60 | syl2anc 584 | . . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ∧ 𝑥 ≠ 𝑦)) → 𝑥 = 〈(1st ‘𝑥), (2nd ‘𝑥)〉) | 
| 90 | 89, 75 | eqeq12d 2752 | . . . . . . . . 9
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ∧ 𝑥 ≠ 𝑦)) → (𝑥 = 𝑦 ↔ 〈(1st ‘𝑥), (2nd ‘𝑥)〉 = 〈(1st
‘𝑦), (2nd
‘𝑦)〉)) | 
| 91 |  | fvex 6918 | . . . . . . . . . 10
⊢
(1st ‘𝑥) ∈ V | 
| 92 |  | fvex 6918 | . . . . . . . . . 10
⊢
(2nd ‘𝑥) ∈ V | 
| 93 | 91, 92 | opth 5480 | . . . . . . . . 9
⊢
(〈(1st ‘𝑥), (2nd ‘𝑥)〉 = 〈(1st ‘𝑦), (2nd ‘𝑦)〉 ↔ ((1st
‘𝑥) = (1st
‘𝑦) ∧
(2nd ‘𝑥) =
(2nd ‘𝑦))) | 
| 94 | 90, 93 | bitrdi 287 | . . . . . . . 8
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ∧ 𝑥 ≠ 𝑦)) → (𝑥 = 𝑦 ↔ ((1st ‘𝑥) = (1st ‘𝑦) ∧ (2nd
‘𝑥) = (2nd
‘𝑦)))) | 
| 95 | 94 | baibd 539 | . . . . . . 7
⊢ (((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ∧ 𝑥 ≠ 𝑦)) ∧ (1st ‘𝑥) = (1st ‘𝑦)) → (𝑥 = 𝑦 ↔ (2nd ‘𝑥) = (2nd ‘𝑦))) | 
| 96 | 95 | necon3bid 2984 | . . . . . 6
⊢ (((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ∧ 𝑥 ≠ 𝑦)) ∧ (1st ‘𝑥) = (1st ‘𝑦)) → (𝑥 ≠ 𝑦 ↔ (2nd ‘𝑥) ≠ (2nd
‘𝑦))) | 
| 97 | 87, 96 | mpbid 232 | . . . . 5
⊢ (((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ∧ 𝑥 ≠ 𝑦)) ∧ (1st ‘𝑥) = (1st ‘𝑦)) → (2nd
‘𝑥) ≠
(2nd ‘𝑦)) | 
| 98 | 55, 59, 71, 86, 97, 1 | dprdcntz 20029 | . . . 4
⊢ (((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ∧ 𝑥 ≠ 𝑦)) ∧ (1st ‘𝑥) = (1st ‘𝑦)) → ((𝑗 ∈ (𝐴 “ {(1st ‘𝑥)}) ↦ ((1st
‘𝑥)𝑆𝑗))‘(2nd ‘𝑥)) ⊆ ((Cntz‘𝐺)‘((𝑗 ∈ (𝐴 “ {(1st ‘𝑥)}) ↦ ((1st
‘𝑥)𝑆𝑗))‘(2nd ‘𝑦)))) | 
| 99 |  | df-ov 7435 | . . . . . 6
⊢
((1st ‘𝑥)𝑆(2nd ‘𝑥)) = (𝑆‘〈(1st ‘𝑥), (2nd ‘𝑥)〉) | 
| 100 |  | oveq2 7440 | . . . . . . . 8
⊢ (𝑗 = (2nd ‘𝑥) → ((1st
‘𝑥)𝑆𝑗) = ((1st ‘𝑥)𝑆(2nd ‘𝑥))) | 
| 101 | 100, 57, 56 | fvmpt3i 7020 | . . . . . . 7
⊢
((2nd ‘𝑥) ∈ (𝐴 “ {(1st ‘𝑥)}) → ((𝑗 ∈ (𝐴 “ {(1st ‘𝑥)}) ↦ ((1st
‘𝑥)𝑆𝑗))‘(2nd ‘𝑥)) = ((1st
‘𝑥)𝑆(2nd ‘𝑥))) | 
| 102 | 70, 101 | syl 17 | . . . . . 6
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ∧ 𝑥 ≠ 𝑦)) → ((𝑗 ∈ (𝐴 “ {(1st ‘𝑥)}) ↦ ((1st
‘𝑥)𝑆𝑗))‘(2nd ‘𝑥)) = ((1st
‘𝑥)𝑆(2nd ‘𝑥))) | 
| 103 | 89 | fveq2d 6909 | . . . . . 6
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ∧ 𝑥 ≠ 𝑦)) → (𝑆‘𝑥) = (𝑆‘〈(1st ‘𝑥), (2nd ‘𝑥)〉)) | 
| 104 | 99, 102, 103 | 3eqtr4a 2802 | . . . . 5
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ∧ 𝑥 ≠ 𝑦)) → ((𝑗 ∈ (𝐴 “ {(1st ‘𝑥)}) ↦ ((1st
‘𝑥)𝑆𝑗))‘(2nd ‘𝑥)) = (𝑆‘𝑥)) | 
| 105 | 104 | adantr 480 | . . . 4
⊢ (((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ∧ 𝑥 ≠ 𝑦)) ∧ (1st ‘𝑥) = (1st ‘𝑦)) → ((𝑗 ∈ (𝐴 “ {(1st ‘𝑥)}) ↦ ((1st
‘𝑥)𝑆𝑗))‘(2nd ‘𝑥)) = (𝑆‘𝑥)) | 
| 106 | 83 | oveq1d 7447 | . . . . . . . 8
⊢ (((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ∧ 𝑥 ≠ 𝑦)) ∧ (1st ‘𝑥) = (1st ‘𝑦)) → ((1st
‘𝑥)𝑆𝑗) = ((1st ‘𝑦)𝑆𝑗)) | 
| 107 | 85, 106 | mpteq12dv 5232 | . . . . . . 7
⊢ (((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ∧ 𝑥 ≠ 𝑦)) ∧ (1st ‘𝑥) = (1st ‘𝑦)) → (𝑗 ∈ (𝐴 “ {(1st ‘𝑥)}) ↦ ((1st
‘𝑥)𝑆𝑗)) = (𝑗 ∈ (𝐴 “ {(1st ‘𝑦)}) ↦ ((1st
‘𝑦)𝑆𝑗))) | 
| 108 | 107 | fveq1d 6907 | . . . . . 6
⊢ (((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ∧ 𝑥 ≠ 𝑦)) ∧ (1st ‘𝑥) = (1st ‘𝑦)) → ((𝑗 ∈ (𝐴 “ {(1st ‘𝑥)}) ↦ ((1st
‘𝑥)𝑆𝑗))‘(2nd ‘𝑦)) = ((𝑗 ∈ (𝐴 “ {(1st ‘𝑦)}) ↦ ((1st
‘𝑦)𝑆𝑗))‘(2nd ‘𝑦))) | 
| 109 |  | df-ov 7435 | . . . . . . . 8
⊢
((1st ‘𝑦)𝑆(2nd ‘𝑦)) = (𝑆‘〈(1st ‘𝑦), (2nd ‘𝑦)〉) | 
| 110 |  | oveq2 7440 | . . . . . . . . . 10
⊢ (𝑗 = (2nd ‘𝑦) → ((1st
‘𝑦)𝑆𝑗) = ((1st ‘𝑦)𝑆(2nd ‘𝑦))) | 
| 111 |  | eqid 2736 | . . . . . . . . . 10
⊢ (𝑗 ∈ (𝐴 “ {(1st ‘𝑦)}) ↦ ((1st
‘𝑦)𝑆𝑗)) = (𝑗 ∈ (𝐴 “ {(1st ‘𝑦)}) ↦ ((1st
‘𝑦)𝑆𝑗)) | 
| 112 |  | ovex 7465 | . . . . . . . . . 10
⊢
((1st ‘𝑦)𝑆𝑗) ∈ V | 
| 113 | 110, 111,
112 | fvmpt3i 7020 | . . . . . . . . 9
⊢
((2nd ‘𝑦) ∈ (𝐴 “ {(1st ‘𝑦)}) → ((𝑗 ∈ (𝐴 “ {(1st ‘𝑦)}) ↦ ((1st
‘𝑦)𝑆𝑗))‘(2nd ‘𝑦)) = ((1st
‘𝑦)𝑆(2nd ‘𝑦))) | 
| 114 | 81, 113 | syl 17 | . . . . . . . 8
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ∧ 𝑥 ≠ 𝑦)) → ((𝑗 ∈ (𝐴 “ {(1st ‘𝑦)}) ↦ ((1st
‘𝑦)𝑆𝑗))‘(2nd ‘𝑦)) = ((1st
‘𝑦)𝑆(2nd ‘𝑦))) | 
| 115 | 75 | fveq2d 6909 | . . . . . . . 8
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ∧ 𝑥 ≠ 𝑦)) → (𝑆‘𝑦) = (𝑆‘〈(1st ‘𝑦), (2nd ‘𝑦)〉)) | 
| 116 | 109, 114,
115 | 3eqtr4a 2802 | . . . . . . 7
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ∧ 𝑥 ≠ 𝑦)) → ((𝑗 ∈ (𝐴 “ {(1st ‘𝑦)}) ↦ ((1st
‘𝑦)𝑆𝑗))‘(2nd ‘𝑦)) = (𝑆‘𝑦)) | 
| 117 | 116 | adantr 480 | . . . . . 6
⊢ (((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ∧ 𝑥 ≠ 𝑦)) ∧ (1st ‘𝑥) = (1st ‘𝑦)) → ((𝑗 ∈ (𝐴 “ {(1st ‘𝑦)}) ↦ ((1st
‘𝑦)𝑆𝑗))‘(2nd ‘𝑦)) = (𝑆‘𝑦)) | 
| 118 | 108, 117 | eqtrd 2776 | . . . . 5
⊢ (((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ∧ 𝑥 ≠ 𝑦)) ∧ (1st ‘𝑥) = (1st ‘𝑦)) → ((𝑗 ∈ (𝐴 “ {(1st ‘𝑥)}) ↦ ((1st
‘𝑥)𝑆𝑗))‘(2nd ‘𝑦)) = (𝑆‘𝑦)) | 
| 119 | 118 | fveq2d 6909 | . . . 4
⊢ (((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ∧ 𝑥 ≠ 𝑦)) ∧ (1st ‘𝑥) = (1st ‘𝑦)) → ((Cntz‘𝐺)‘((𝑗 ∈ (𝐴 “ {(1st ‘𝑥)}) ↦ ((1st
‘𝑥)𝑆𝑗))‘(2nd ‘𝑦))) = ((Cntz‘𝐺)‘(𝑆‘𝑦))) | 
| 120 | 98, 105, 119 | 3sstr3d 4037 | . . 3
⊢ (((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ∧ 𝑥 ≠ 𝑦)) ∧ (1st ‘𝑥) = (1st ‘𝑦)) → (𝑆‘𝑥) ⊆ ((Cntz‘𝐺)‘(𝑆‘𝑦))) | 
| 121 | 11, 41, 12, 29, 4, 3 | dprd2dlem2 20061 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝑆‘𝑥) ⊆ (𝐺 DProd (𝑗 ∈ (𝐴 “ {(1st ‘𝑥)}) ↦ ((1st
‘𝑥)𝑆𝑗)))) | 
| 122 | 45 | oveq2d 7448 | . . . . . . . . 9
⊢ (𝑖 = (1st ‘𝑥) → (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗))) = (𝐺 DProd (𝑗 ∈ (𝐴 “ {(1st ‘𝑥)}) ↦ ((1st
‘𝑥)𝑆𝑗)))) | 
| 123 | 122, 17, 16 | fvmpt3i 7020 | . . . . . . . 8
⊢
((1st ‘𝑥) ∈ 𝐼 → ((𝑖 ∈ 𝐼 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗))))‘(1st ‘𝑥)) = (𝐺 DProd (𝑗 ∈ (𝐴 “ {(1st ‘𝑥)}) ↦ ((1st
‘𝑥)𝑆𝑗)))) | 
| 124 | 52, 123 | syl 17 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → ((𝑖 ∈ 𝐼 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗))))‘(1st ‘𝑥)) = (𝐺 DProd (𝑗 ∈ (𝐴 “ {(1st ‘𝑥)}) ↦ ((1st
‘𝑥)𝑆𝑗)))) | 
| 125 | 121, 124 | sseqtrrd 4020 | . . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝑆‘𝑥) ⊆ ((𝑖 ∈ 𝐼 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗))))‘(1st ‘𝑥))) | 
| 126 | 125 | 3ad2antr1 1188 | . . . . 5
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ∧ 𝑥 ≠ 𝑦)) → (𝑆‘𝑥) ⊆ ((𝑖 ∈ 𝐼 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗))))‘(1st ‘𝑥))) | 
| 127 | 126 | adantr 480 | . . . 4
⊢ (((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ∧ 𝑥 ≠ 𝑦)) ∧ (1st ‘𝑥) ≠ (1st
‘𝑦)) → (𝑆‘𝑥) ⊆ ((𝑖 ∈ 𝐼 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗))))‘(1st ‘𝑥))) | 
| 128 | 4 | ad2antrr 726 | . . . . . 6
⊢ (((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ∧ 𝑥 ≠ 𝑦)) ∧ (1st ‘𝑥) ≠ (1st
‘𝑦)) → 𝐺dom DProd (𝑖 ∈ 𝐼 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗))))) | 
| 129 | 18 | a1i 11 | . . . . . 6
⊢ (((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ∧ 𝑥 ≠ 𝑦)) ∧ (1st ‘𝑥) ≠ (1st
‘𝑦)) → dom
(𝑖 ∈ 𝐼 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗)))) = 𝐼) | 
| 130 | 52 | 3ad2antr1 1188 | . . . . . . 7
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ∧ 𝑥 ≠ 𝑦)) → (1st ‘𝑥) ∈ 𝐼) | 
| 131 | 130 | adantr 480 | . . . . . 6
⊢ (((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ∧ 𝑥 ≠ 𝑦)) ∧ (1st ‘𝑥) ≠ (1st
‘𝑦)) →
(1st ‘𝑥)
∈ 𝐼) | 
| 132 | 12 | adantr 480 | . . . . . . . 8
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ∧ 𝑥 ≠ 𝑦)) → dom 𝐴 ⊆ 𝐼) | 
| 133 |  | 1stdm 8066 | . . . . . . . . 9
⊢ ((Rel
𝐴 ∧ 𝑦 ∈ 𝐴) → (1st ‘𝑦) ∈ dom 𝐴) | 
| 134 | 72, 73, 133 | syl2anc 584 | . . . . . . . 8
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ∧ 𝑥 ≠ 𝑦)) → (1st ‘𝑦) ∈ dom 𝐴) | 
| 135 | 132, 134 | sseldd 3983 | . . . . . . 7
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ∧ 𝑥 ≠ 𝑦)) → (1st ‘𝑦) ∈ 𝐼) | 
| 136 | 135 | adantr 480 | . . . . . 6
⊢ (((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ∧ 𝑥 ≠ 𝑦)) ∧ (1st ‘𝑥) ≠ (1st
‘𝑦)) →
(1st ‘𝑦)
∈ 𝐼) | 
| 137 |  | simpr 484 | . . . . . 6
⊢ (((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ∧ 𝑥 ≠ 𝑦)) ∧ (1st ‘𝑥) ≠ (1st
‘𝑦)) →
(1st ‘𝑥)
≠ (1st ‘𝑦)) | 
| 138 | 128, 129,
131, 136, 137, 1 | dprdcntz 20029 | . . . . 5
⊢ (((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ∧ 𝑥 ≠ 𝑦)) ∧ (1st ‘𝑥) ≠ (1st
‘𝑦)) → ((𝑖 ∈ 𝐼 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗))))‘(1st ‘𝑥)) ⊆ ((Cntz‘𝐺)‘((𝑖 ∈ 𝐼 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗))))‘(1st ‘𝑦)))) | 
| 139 |  | sneq 4635 | . . . . . . . . . . . . 13
⊢ (𝑖 = (1st ‘𝑦) → {𝑖} = {(1st ‘𝑦)}) | 
| 140 | 139 | imaeq2d 6077 | . . . . . . . . . . . 12
⊢ (𝑖 = (1st ‘𝑦) → (𝐴 “ {𝑖}) = (𝐴 “ {(1st ‘𝑦)})) | 
| 141 |  | oveq1 7439 | . . . . . . . . . . . 12
⊢ (𝑖 = (1st ‘𝑦) → (𝑖𝑆𝑗) = ((1st ‘𝑦)𝑆𝑗)) | 
| 142 | 140, 141 | mpteq12dv 5232 | . . . . . . . . . . 11
⊢ (𝑖 = (1st ‘𝑦) → (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗)) = (𝑗 ∈ (𝐴 “ {(1st ‘𝑦)}) ↦ ((1st
‘𝑦)𝑆𝑗))) | 
| 143 | 142 | oveq2d 7448 | . . . . . . . . . 10
⊢ (𝑖 = (1st ‘𝑦) → (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗))) = (𝐺 DProd (𝑗 ∈ (𝐴 “ {(1st ‘𝑦)}) ↦ ((1st
‘𝑦)𝑆𝑗)))) | 
| 144 | 143, 17, 16 | fvmpt3i 7020 | . . . . . . . . 9
⊢
((1st ‘𝑦) ∈ 𝐼 → ((𝑖 ∈ 𝐼 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗))))‘(1st ‘𝑦)) = (𝐺 DProd (𝑗 ∈ (𝐴 “ {(1st ‘𝑦)}) ↦ ((1st
‘𝑦)𝑆𝑗)))) | 
| 145 | 135, 144 | syl 17 | . . . . . . . 8
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ∧ 𝑥 ≠ 𝑦)) → ((𝑖 ∈ 𝐼 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗))))‘(1st ‘𝑦)) = (𝐺 DProd (𝑗 ∈ (𝐴 “ {(1st ‘𝑦)}) ↦ ((1st
‘𝑦)𝑆𝑗)))) | 
| 146 | 145 | fveq2d 6909 | . . . . . . 7
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ∧ 𝑥 ≠ 𝑦)) → ((Cntz‘𝐺)‘((𝑖 ∈ 𝐼 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗))))‘(1st ‘𝑦))) = ((Cntz‘𝐺)‘(𝐺 DProd (𝑗 ∈ (𝐴 “ {(1st ‘𝑦)}) ↦ ((1st
‘𝑦)𝑆𝑗))))) | 
| 147 |  | eqid 2736 | . . . . . . . . 9
⊢
(Base‘𝐺) =
(Base‘𝐺) | 
| 148 | 147 | dprdssv 20037 | . . . . . . . 8
⊢ (𝐺 DProd (𝑗 ∈ (𝐴 “ {(1st ‘𝑦)}) ↦ ((1st
‘𝑦)𝑆𝑗))) ⊆ (Base‘𝐺) | 
| 149 | 142 | breq2d 5154 | . . . . . . . . . . 11
⊢ (𝑖 = (1st ‘𝑦) → (𝐺dom DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗)) ↔ 𝐺dom DProd (𝑗 ∈ (𝐴 “ {(1st ‘𝑦)}) ↦ ((1st
‘𝑦)𝑆𝑗)))) | 
| 150 | 47 | adantr 480 | . . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ∧ 𝑥 ≠ 𝑦)) → ∀𝑖 ∈ 𝐼 𝐺dom DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗))) | 
| 151 | 149, 150,
135 | rspcdva 3622 | . . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ∧ 𝑥 ≠ 𝑦)) → 𝐺dom DProd (𝑗 ∈ (𝐴 “ {(1st ‘𝑦)}) ↦ ((1st
‘𝑦)𝑆𝑗))) | 
| 152 | 112, 111 | dmmpti 6711 | . . . . . . . . . . 11
⊢ dom
(𝑗 ∈ (𝐴 “ {(1st
‘𝑦)}) ↦
((1st ‘𝑦)𝑆𝑗)) = (𝐴 “ {(1st ‘𝑦)}) | 
| 153 | 152 | a1i 11 | . . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ∧ 𝑥 ≠ 𝑦)) → dom (𝑗 ∈ (𝐴 “ {(1st ‘𝑦)}) ↦ ((1st
‘𝑦)𝑆𝑗)) = (𝐴 “ {(1st ‘𝑦)})) | 
| 154 | 151, 153,
81 | dprdub 20046 | . . . . . . . . 9
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ∧ 𝑥 ≠ 𝑦)) → ((𝑗 ∈ (𝐴 “ {(1st ‘𝑦)}) ↦ ((1st
‘𝑦)𝑆𝑗))‘(2nd ‘𝑦)) ⊆ (𝐺 DProd (𝑗 ∈ (𝐴 “ {(1st ‘𝑦)}) ↦ ((1st
‘𝑦)𝑆𝑗)))) | 
| 155 | 116, 154 | eqsstrrd 4018 | . . . . . . . 8
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ∧ 𝑥 ≠ 𝑦)) → (𝑆‘𝑦) ⊆ (𝐺 DProd (𝑗 ∈ (𝐴 “ {(1st ‘𝑦)}) ↦ ((1st
‘𝑦)𝑆𝑗)))) | 
| 156 | 147, 1 | cntz2ss 19354 | . . . . . . . 8
⊢ (((𝐺 DProd (𝑗 ∈ (𝐴 “ {(1st ‘𝑦)}) ↦ ((1st
‘𝑦)𝑆𝑗))) ⊆ (Base‘𝐺) ∧ (𝑆‘𝑦) ⊆ (𝐺 DProd (𝑗 ∈ (𝐴 “ {(1st ‘𝑦)}) ↦ ((1st
‘𝑦)𝑆𝑗)))) → ((Cntz‘𝐺)‘(𝐺 DProd (𝑗 ∈ (𝐴 “ {(1st ‘𝑦)}) ↦ ((1st
‘𝑦)𝑆𝑗)))) ⊆ ((Cntz‘𝐺)‘(𝑆‘𝑦))) | 
| 157 | 148, 155,
156 | sylancr 587 | . . . . . . 7
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ∧ 𝑥 ≠ 𝑦)) → ((Cntz‘𝐺)‘(𝐺 DProd (𝑗 ∈ (𝐴 “ {(1st ‘𝑦)}) ↦ ((1st
‘𝑦)𝑆𝑗)))) ⊆ ((Cntz‘𝐺)‘(𝑆‘𝑦))) | 
| 158 | 146, 157 | eqsstrd 4017 | . . . . . 6
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ∧ 𝑥 ≠ 𝑦)) → ((Cntz‘𝐺)‘((𝑖 ∈ 𝐼 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗))))‘(1st ‘𝑦))) ⊆ ((Cntz‘𝐺)‘(𝑆‘𝑦))) | 
| 159 | 158 | adantr 480 | . . . . 5
⊢ (((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ∧ 𝑥 ≠ 𝑦)) ∧ (1st ‘𝑥) ≠ (1st
‘𝑦)) →
((Cntz‘𝐺)‘((𝑖 ∈ 𝐼 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗))))‘(1st ‘𝑦))) ⊆ ((Cntz‘𝐺)‘(𝑆‘𝑦))) | 
| 160 | 138, 159 | sstrd 3993 | . . . 4
⊢ (((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ∧ 𝑥 ≠ 𝑦)) ∧ (1st ‘𝑥) ≠ (1st
‘𝑦)) → ((𝑖 ∈ 𝐼 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗))))‘(1st ‘𝑥)) ⊆ ((Cntz‘𝐺)‘(𝑆‘𝑦))) | 
| 161 | 127, 160 | sstrd 3993 | . . 3
⊢ (((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ∧ 𝑥 ≠ 𝑦)) ∧ (1st ‘𝑥) ≠ (1st
‘𝑦)) → (𝑆‘𝑥) ⊆ ((Cntz‘𝐺)‘(𝑆‘𝑦))) | 
| 162 | 120, 161 | pm2.61dane 3028 | . 2
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ∧ 𝑥 ≠ 𝑦)) → (𝑆‘𝑥) ⊆ ((Cntz‘𝐺)‘(𝑆‘𝑦))) | 
| 163 | 6 | adantr 480 | . . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐺 ∈ Grp) | 
| 164 | 147 | subgacs 19180 | . . . . . 6
⊢ (𝐺 ∈ Grp →
(SubGrp‘𝐺) ∈
(ACS‘(Base‘𝐺))) | 
| 165 |  | acsmre 17696 | . . . . . 6
⊢
((SubGrp‘𝐺)
∈ (ACS‘(Base‘𝐺)) → (SubGrp‘𝐺) ∈ (Moore‘(Base‘𝐺))) | 
| 166 | 163, 164,
165 | 3syl 18 | . . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (SubGrp‘𝐺) ∈ (Moore‘(Base‘𝐺))) | 
| 167 | 14 | adantr 480 | . . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝐴 ↾ 𝐼) = 𝐴) | 
| 168 |  | undif2 4476 | . . . . . . . . . . . . . . . . . 18
⊢
({(1st ‘𝑥)} ∪ (𝐼 ∖ {(1st ‘𝑥)})) = ({(1st
‘𝑥)} ∪ 𝐼) | 
| 169 | 52 | snssd 4808 | . . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → {(1st ‘𝑥)} ⊆ 𝐼) | 
| 170 |  | ssequn1 4185 | . . . . . . . . . . . . . . . . . . 19
⊢
({(1st ‘𝑥)} ⊆ 𝐼 ↔ ({(1st ‘𝑥)} ∪ 𝐼) = 𝐼) | 
| 171 | 169, 170 | sylib 218 | . . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → ({(1st ‘𝑥)} ∪ 𝐼) = 𝐼) | 
| 172 | 168, 171 | eqtr2id 2789 | . . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐼 = ({(1st ‘𝑥)} ∪ (𝐼 ∖ {(1st ‘𝑥)}))) | 
| 173 | 172 | reseq2d 5996 | . . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝐴 ↾ 𝐼) = (𝐴 ↾ ({(1st ‘𝑥)} ∪ (𝐼 ∖ {(1st ‘𝑥)})))) | 
| 174 | 167, 173 | eqtr3d 2778 | . . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐴 = (𝐴 ↾ ({(1st ‘𝑥)} ∪ (𝐼 ∖ {(1st ‘𝑥)})))) | 
| 175 |  | resundi 6010 | . . . . . . . . . . . . . . 15
⊢ (𝐴 ↾ ({(1st
‘𝑥)} ∪ (𝐼 ∖ {(1st
‘𝑥)}))) = ((𝐴 ↾ {(1st
‘𝑥)}) ∪ (𝐴 ↾ (𝐼 ∖ {(1st ‘𝑥)}))) | 
| 176 | 174, 175 | eqtrdi 2792 | . . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐴 = ((𝐴 ↾ {(1st ‘𝑥)}) ∪ (𝐴 ↾ (𝐼 ∖ {(1st ‘𝑥)})))) | 
| 177 | 176 | difeq1d 4124 | . . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝐴 ∖ {𝑥}) = (((𝐴 ↾ {(1st ‘𝑥)}) ∪ (𝐴 ↾ (𝐼 ∖ {(1st ‘𝑥)}))) ∖ {𝑥})) | 
| 178 |  | difundir 4290 | . . . . . . . . . . . . 13
⊢ (((𝐴 ↾ {(1st
‘𝑥)}) ∪ (𝐴 ↾ (𝐼 ∖ {(1st ‘𝑥)}))) ∖ {𝑥}) = (((𝐴 ↾ {(1st ‘𝑥)}) ∖ {𝑥}) ∪ ((𝐴 ↾ (𝐼 ∖ {(1st ‘𝑥)})) ∖ {𝑥})) | 
| 179 | 177, 178 | eqtrdi 2792 | . . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝐴 ∖ {𝑥}) = (((𝐴 ↾ {(1st ‘𝑥)}) ∖ {𝑥}) ∪ ((𝐴 ↾ (𝐼 ∖ {(1st ‘𝑥)})) ∖ {𝑥}))) | 
| 180 |  | neirr 2948 | . . . . . . . . . . . . . . . . 17
⊢  ¬
(1st ‘𝑥)
≠ (1st ‘𝑥) | 
| 181 | 61 | eleq1d 2825 | . . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝑥 ∈ (𝐴 ↾ (𝐼 ∖ {(1st ‘𝑥)})) ↔
〈(1st ‘𝑥), (2nd ‘𝑥)〉 ∈ (𝐴 ↾ (𝐼 ∖ {(1st ‘𝑥)})))) | 
| 182 |  | df-br 5143 | . . . . . . . . . . . . . . . . . . 19
⊢
((1st ‘𝑥)(𝐴 ↾ (𝐼 ∖ {(1st ‘𝑥)}))(2nd ‘𝑥) ↔ 〈(1st
‘𝑥), (2nd
‘𝑥)〉 ∈
(𝐴 ↾ (𝐼 ∖ {(1st
‘𝑥)}))) | 
| 183 | 92 | brresi 6005 | . . . . . . . . . . . . . . . . . . . . 21
⊢
((1st ‘𝑥)(𝐴 ↾ (𝐼 ∖ {(1st ‘𝑥)}))(2nd ‘𝑥) ↔ ((1st
‘𝑥) ∈ (𝐼 ∖ {(1st
‘𝑥)}) ∧
(1st ‘𝑥)𝐴(2nd ‘𝑥))) | 
| 184 | 183 | simplbi 497 | . . . . . . . . . . . . . . . . . . . 20
⊢
((1st ‘𝑥)(𝐴 ↾ (𝐼 ∖ {(1st ‘𝑥)}))(2nd ‘𝑥) → (1st
‘𝑥) ∈ (𝐼 ∖ {(1st
‘𝑥)})) | 
| 185 |  | eldifsni 4789 | . . . . . . . . . . . . . . . . . . . 20
⊢
((1st ‘𝑥) ∈ (𝐼 ∖ {(1st ‘𝑥)}) → (1st
‘𝑥) ≠
(1st ‘𝑥)) | 
| 186 | 184, 185 | syl 17 | . . . . . . . . . . . . . . . . . . 19
⊢
((1st ‘𝑥)(𝐴 ↾ (𝐼 ∖ {(1st ‘𝑥)}))(2nd ‘𝑥) → (1st
‘𝑥) ≠
(1st ‘𝑥)) | 
| 187 | 182, 186 | sylbir 235 | . . . . . . . . . . . . . . . . . 18
⊢
(〈(1st ‘𝑥), (2nd ‘𝑥)〉 ∈ (𝐴 ↾ (𝐼 ∖ {(1st ‘𝑥)})) → (1st
‘𝑥) ≠
(1st ‘𝑥)) | 
| 188 | 181, 187 | biimtrdi 253 | . . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝑥 ∈ (𝐴 ↾ (𝐼 ∖ {(1st ‘𝑥)})) → (1st
‘𝑥) ≠
(1st ‘𝑥))) | 
| 189 | 180, 188 | mtoi 199 | . . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → ¬ 𝑥 ∈ (𝐴 ↾ (𝐼 ∖ {(1st ‘𝑥)}))) | 
| 190 |  | disjsn 4710 | . . . . . . . . . . . . . . . 16
⊢ (((𝐴 ↾ (𝐼 ∖ {(1st ‘𝑥)})) ∩ {𝑥}) = ∅ ↔ ¬ 𝑥 ∈ (𝐴 ↾ (𝐼 ∖ {(1st ‘𝑥)}))) | 
| 191 | 189, 190 | sylibr 234 | . . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → ((𝐴 ↾ (𝐼 ∖ {(1st ‘𝑥)})) ∩ {𝑥}) = ∅) | 
| 192 |  | disj3 4453 | . . . . . . . . . . . . . . 15
⊢ (((𝐴 ↾ (𝐼 ∖ {(1st ‘𝑥)})) ∩ {𝑥}) = ∅ ↔ (𝐴 ↾ (𝐼 ∖ {(1st ‘𝑥)})) = ((𝐴 ↾ (𝐼 ∖ {(1st ‘𝑥)})) ∖ {𝑥})) | 
| 193 | 191, 192 | sylib 218 | . . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝐴 ↾ (𝐼 ∖ {(1st ‘𝑥)})) = ((𝐴 ↾ (𝐼 ∖ {(1st ‘𝑥)})) ∖ {𝑥})) | 
| 194 | 193 | eqcomd 2742 | . . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → ((𝐴 ↾ (𝐼 ∖ {(1st ‘𝑥)})) ∖ {𝑥}) = (𝐴 ↾ (𝐼 ∖ {(1st ‘𝑥)}))) | 
| 195 | 194 | uneq2d 4167 | . . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (((𝐴 ↾ {(1st ‘𝑥)}) ∖ {𝑥}) ∪ ((𝐴 ↾ (𝐼 ∖ {(1st ‘𝑥)})) ∖ {𝑥})) = (((𝐴 ↾ {(1st ‘𝑥)}) ∖ {𝑥}) ∪ (𝐴 ↾ (𝐼 ∖ {(1st ‘𝑥)})))) | 
| 196 | 179, 195 | eqtrd 2776 | . . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝐴 ∖ {𝑥}) = (((𝐴 ↾ {(1st ‘𝑥)}) ∖ {𝑥}) ∪ (𝐴 ↾ (𝐼 ∖ {(1st ‘𝑥)})))) | 
| 197 | 196 | imaeq2d 6077 | . . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝑆 “ (𝐴 ∖ {𝑥})) = (𝑆 “ (((𝐴 ↾ {(1st ‘𝑥)}) ∖ {𝑥}) ∪ (𝐴 ↾ (𝐼 ∖ {(1st ‘𝑥)}))))) | 
| 198 |  | imaundi 6168 | . . . . . . . . . 10
⊢ (𝑆 “ (((𝐴 ↾ {(1st ‘𝑥)}) ∖ {𝑥}) ∪ (𝐴 ↾ (𝐼 ∖ {(1st ‘𝑥)})))) = ((𝑆 “ ((𝐴 ↾ {(1st ‘𝑥)}) ∖ {𝑥})) ∪ (𝑆 “ (𝐴 ↾ (𝐼 ∖ {(1st ‘𝑥)})))) | 
| 199 | 197, 198 | eqtrdi 2792 | . . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝑆 “ (𝐴 ∖ {𝑥})) = ((𝑆 “ ((𝐴 ↾ {(1st ‘𝑥)}) ∖ {𝑥})) ∪ (𝑆 “ (𝐴 ↾ (𝐼 ∖ {(1st ‘𝑥)}))))) | 
| 200 | 199 | unieqd 4919 | . . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → ∪ (𝑆 “ (𝐴 ∖ {𝑥})) = ∪ ((𝑆 “ ((𝐴 ↾ {(1st ‘𝑥)}) ∖ {𝑥})) ∪ (𝑆 “ (𝐴 ↾ (𝐼 ∖ {(1st ‘𝑥)}))))) | 
| 201 |  | uniun 4929 | . . . . . . . 8
⊢ ∪ ((𝑆
“ ((𝐴 ↾
{(1st ‘𝑥)}) ∖ {𝑥})) ∪ (𝑆 “ (𝐴 ↾ (𝐼 ∖ {(1st ‘𝑥)})))) = (∪ (𝑆
“ ((𝐴 ↾
{(1st ‘𝑥)}) ∖ {𝑥})) ∪ ∪ (𝑆 “ (𝐴 ↾ (𝐼 ∖ {(1st ‘𝑥)})))) | 
| 202 | 200, 201 | eqtrdi 2792 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → ∪ (𝑆 “ (𝐴 ∖ {𝑥})) = (∪ (𝑆 “ ((𝐴 ↾ {(1st ‘𝑥)}) ∖ {𝑥})) ∪ ∪ (𝑆 “ (𝐴 ↾ (𝐼 ∖ {(1st ‘𝑥)}))))) | 
| 203 |  | imassrn 6088 | . . . . . . . . . . 11
⊢ (𝑆 “ ((𝐴 ↾ {(1st ‘𝑥)}) ∖ {𝑥})) ⊆ ran 𝑆 | 
| 204 | 41 | frnd 6743 | . . . . . . . . . . . . 13
⊢ (𝜑 → ran 𝑆 ⊆ (SubGrp‘𝐺)) | 
| 205 | 204 | adantr 480 | . . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → ran 𝑆 ⊆ (SubGrp‘𝐺)) | 
| 206 |  | mresspw 17636 | . . . . . . . . . . . . 13
⊢
((SubGrp‘𝐺)
∈ (Moore‘(Base‘𝐺)) → (SubGrp‘𝐺) ⊆ 𝒫 (Base‘𝐺)) | 
| 207 | 166, 206 | syl 17 | . . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (SubGrp‘𝐺) ⊆ 𝒫 (Base‘𝐺)) | 
| 208 | 205, 207 | sstrd 3993 | . . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → ran 𝑆 ⊆ 𝒫 (Base‘𝐺)) | 
| 209 | 203, 208 | sstrid 3994 | . . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝑆 “ ((𝐴 ↾ {(1st ‘𝑥)}) ∖ {𝑥})) ⊆ 𝒫 (Base‘𝐺)) | 
| 210 |  | sspwuni 5099 | . . . . . . . . . 10
⊢ ((𝑆 “ ((𝐴 ↾ {(1st ‘𝑥)}) ∖ {𝑥})) ⊆ 𝒫 (Base‘𝐺) ↔ ∪ (𝑆
“ ((𝐴 ↾
{(1st ‘𝑥)}) ∖ {𝑥})) ⊆ (Base‘𝐺)) | 
| 211 | 209, 210 | sylib 218 | . . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → ∪ (𝑆 “ ((𝐴 ↾ {(1st ‘𝑥)}) ∖ {𝑥})) ⊆ (Base‘𝐺)) | 
| 212 | 166, 3, 211 | mrcssidd 17669 | . . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → ∪ (𝑆 “ ((𝐴 ↾ {(1st ‘𝑥)}) ∖ {𝑥})) ⊆ (𝐾‘∪ (𝑆 “ ((𝐴 ↾ {(1st ‘𝑥)}) ∖ {𝑥})))) | 
| 213 |  | imassrn 6088 | . . . . . . . . . . 11
⊢ (𝑆 “ (𝐴 ↾ (𝐼 ∖ {(1st ‘𝑥)}))) ⊆ ran 𝑆 | 
| 214 | 213, 208 | sstrid 3994 | . . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝑆 “ (𝐴 ↾ (𝐼 ∖ {(1st ‘𝑥)}))) ⊆ 𝒫
(Base‘𝐺)) | 
| 215 |  | sspwuni 5099 | . . . . . . . . . 10
⊢ ((𝑆 “ (𝐴 ↾ (𝐼 ∖ {(1st ‘𝑥)}))) ⊆ 𝒫
(Base‘𝐺) ↔ ∪ (𝑆
“ (𝐴 ↾ (𝐼 ∖ {(1st
‘𝑥)}))) ⊆
(Base‘𝐺)) | 
| 216 | 214, 215 | sylib 218 | . . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → ∪ (𝑆 “ (𝐴 ↾ (𝐼 ∖ {(1st ‘𝑥)}))) ⊆ (Base‘𝐺)) | 
| 217 | 166, 3, 216 | mrcssidd 17669 | . . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → ∪ (𝑆 “ (𝐴 ↾ (𝐼 ∖ {(1st ‘𝑥)}))) ⊆ (𝐾‘∪ (𝑆 “ (𝐴 ↾ (𝐼 ∖ {(1st ‘𝑥)}))))) | 
| 218 |  | unss12 4187 | . . . . . . . 8
⊢ ((∪ (𝑆
“ ((𝐴 ↾
{(1st ‘𝑥)}) ∖ {𝑥})) ⊆ (𝐾‘∪ (𝑆 “ ((𝐴 ↾ {(1st ‘𝑥)}) ∖ {𝑥}))) ∧ ∪
(𝑆 “ (𝐴 ↾ (𝐼 ∖ {(1st ‘𝑥)}))) ⊆ (𝐾‘∪ (𝑆 “ (𝐴 ↾ (𝐼 ∖ {(1st ‘𝑥)}))))) → (∪ (𝑆
“ ((𝐴 ↾
{(1st ‘𝑥)}) ∖ {𝑥})) ∪ ∪ (𝑆 “ (𝐴 ↾ (𝐼 ∖ {(1st ‘𝑥)})))) ⊆ ((𝐾‘∪ (𝑆
“ ((𝐴 ↾
{(1st ‘𝑥)}) ∖ {𝑥}))) ∪ (𝐾‘∪ (𝑆 “ (𝐴 ↾ (𝐼 ∖ {(1st ‘𝑥)})))))) | 
| 219 | 212, 217,
218 | syl2anc 584 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (∪
(𝑆 “ ((𝐴 ↾ {(1st
‘𝑥)}) ∖ {𝑥})) ∪ ∪ (𝑆
“ (𝐴 ↾ (𝐼 ∖ {(1st
‘𝑥)})))) ⊆
((𝐾‘∪ (𝑆
“ ((𝐴 ↾
{(1st ‘𝑥)}) ∖ {𝑥}))) ∪ (𝐾‘∪ (𝑆 “ (𝐴 ↾ (𝐼 ∖ {(1st ‘𝑥)})))))) | 
| 220 | 202, 219 | eqsstrd 4017 | . . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → ∪ (𝑆 “ (𝐴 ∖ {𝑥})) ⊆ ((𝐾‘∪ (𝑆 “ ((𝐴 ↾ {(1st ‘𝑥)}) ∖ {𝑥}))) ∪ (𝐾‘∪ (𝑆 “ (𝐴 ↾ (𝐼 ∖ {(1st ‘𝑥)})))))) | 
| 221 | 3 | mrccl 17655 | . . . . . . . 8
⊢
(((SubGrp‘𝐺)
∈ (Moore‘(Base‘𝐺)) ∧ ∪ (𝑆 “ ((𝐴 ↾ {(1st ‘𝑥)}) ∖ {𝑥})) ⊆ (Base‘𝐺)) → (𝐾‘∪ (𝑆 “ ((𝐴 ↾ {(1st ‘𝑥)}) ∖ {𝑥}))) ∈ (SubGrp‘𝐺)) | 
| 222 | 166, 211,
221 | syl2anc 584 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝐾‘∪ (𝑆 “ ((𝐴 ↾ {(1st ‘𝑥)}) ∖ {𝑥}))) ∈ (SubGrp‘𝐺)) | 
| 223 | 3 | mrccl 17655 | . . . . . . . 8
⊢
(((SubGrp‘𝐺)
∈ (Moore‘(Base‘𝐺)) ∧ ∪ (𝑆 “ (𝐴 ↾ (𝐼 ∖ {(1st ‘𝑥)}))) ⊆ (Base‘𝐺)) → (𝐾‘∪ (𝑆 “ (𝐴 ↾ (𝐼 ∖ {(1st ‘𝑥)})))) ∈
(SubGrp‘𝐺)) | 
| 224 | 166, 216,
223 | syl2anc 584 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝐾‘∪ (𝑆 “ (𝐴 ↾ (𝐼 ∖ {(1st ‘𝑥)})))) ∈
(SubGrp‘𝐺)) | 
| 225 |  | eqid 2736 | . . . . . . . 8
⊢
(LSSum‘𝐺) =
(LSSum‘𝐺) | 
| 226 | 225 | lsmunss 19678 | . . . . . . 7
⊢ (((𝐾‘∪ (𝑆
“ ((𝐴 ↾
{(1st ‘𝑥)}) ∖ {𝑥}))) ∈ (SubGrp‘𝐺) ∧ (𝐾‘∪ (𝑆 “ (𝐴 ↾ (𝐼 ∖ {(1st ‘𝑥)})))) ∈
(SubGrp‘𝐺)) →
((𝐾‘∪ (𝑆
“ ((𝐴 ↾
{(1st ‘𝑥)}) ∖ {𝑥}))) ∪ (𝐾‘∪ (𝑆 “ (𝐴 ↾ (𝐼 ∖ {(1st ‘𝑥)}))))) ⊆ ((𝐾‘∪ (𝑆
“ ((𝐴 ↾
{(1st ‘𝑥)}) ∖ {𝑥})))(LSSum‘𝐺)(𝐾‘∪ (𝑆 “ (𝐴 ↾ (𝐼 ∖ {(1st ‘𝑥)})))))) | 
| 227 | 222, 224,
226 | syl2anc 584 | . . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → ((𝐾‘∪ (𝑆 “ ((𝐴 ↾ {(1st ‘𝑥)}) ∖ {𝑥}))) ∪ (𝐾‘∪ (𝑆 “ (𝐴 ↾ (𝐼 ∖ {(1st ‘𝑥)}))))) ⊆ ((𝐾‘∪ (𝑆
“ ((𝐴 ↾
{(1st ‘𝑥)}) ∖ {𝑥})))(LSSum‘𝐺)(𝐾‘∪ (𝑆 “ (𝐴 ↾ (𝐼 ∖ {(1st ‘𝑥)})))))) | 
| 228 | 220, 227 | sstrd 3993 | . . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → ∪ (𝑆 “ (𝐴 ∖ {𝑥})) ⊆ ((𝐾‘∪ (𝑆 “ ((𝐴 ↾ {(1st ‘𝑥)}) ∖ {𝑥})))(LSSum‘𝐺)(𝐾‘∪ (𝑆 “ (𝐴 ↾ (𝐼 ∖ {(1st ‘𝑥)})))))) | 
| 229 |  | difss 4135 | . . . . . . . . . . . . 13
⊢ ((𝐴 ↾ {(1st
‘𝑥)}) ∖ {𝑥}) ⊆ (𝐴 ↾ {(1st ‘𝑥)}) | 
| 230 |  | ressn 6304 | . . . . . . . . . . . . 13
⊢ (𝐴 ↾ {(1st
‘𝑥)}) =
({(1st ‘𝑥)} × (𝐴 “ {(1st ‘𝑥)})) | 
| 231 | 229, 230 | sseqtri 4031 | . . . . . . . . . . . 12
⊢ ((𝐴 ↾ {(1st
‘𝑥)}) ∖ {𝑥}) ⊆ ({(1st
‘𝑥)} × (𝐴 “ {(1st
‘𝑥)})) | 
| 232 |  | imass2 6119 | . . . . . . . . . . . 12
⊢ (((𝐴 ↾ {(1st
‘𝑥)}) ∖ {𝑥}) ⊆ ({(1st
‘𝑥)} × (𝐴 “ {(1st
‘𝑥)})) → (𝑆 “ ((𝐴 ↾ {(1st ‘𝑥)}) ∖ {𝑥})) ⊆ (𝑆 “ ({(1st ‘𝑥)} × (𝐴 “ {(1st ‘𝑥)})))) | 
| 233 | 231, 232 | ax-mp 5 | . . . . . . . . . . 11
⊢ (𝑆 “ ((𝐴 ↾ {(1st ‘𝑥)}) ∖ {𝑥})) ⊆ (𝑆 “ ({(1st ‘𝑥)} × (𝐴 “ {(1st ‘𝑥)}))) | 
| 234 |  | ovex 7465 | . . . . . . . . . . . . . . . 16
⊢
((1st ‘𝑥)𝑆𝑖) ∈ V | 
| 235 |  | oveq2 7440 | . . . . . . . . . . . . . . . . 17
⊢ (𝑗 = 𝑖 → ((1st ‘𝑥)𝑆𝑗) = ((1st ‘𝑥)𝑆𝑖)) | 
| 236 | 57, 235 | elrnmpt1s 5969 | . . . . . . . . . . . . . . . 16
⊢ ((𝑖 ∈ (𝐴 “ {(1st ‘𝑥)}) ∧ ((1st
‘𝑥)𝑆𝑖) ∈ V) → ((1st
‘𝑥)𝑆𝑖) ∈ ran (𝑗 ∈ (𝐴 “ {(1st ‘𝑥)}) ↦ ((1st
‘𝑥)𝑆𝑗))) | 
| 237 | 234, 236 | mpan2 691 | . . . . . . . . . . . . . . 15
⊢ (𝑖 ∈ (𝐴 “ {(1st ‘𝑥)}) → ((1st
‘𝑥)𝑆𝑖) ∈ ran (𝑗 ∈ (𝐴 “ {(1st ‘𝑥)}) ↦ ((1st
‘𝑥)𝑆𝑗))) | 
| 238 | 237 | rgen 3062 | . . . . . . . . . . . . . 14
⊢
∀𝑖 ∈
(𝐴 “ {(1st
‘𝑥)})((1st
‘𝑥)𝑆𝑖) ∈ ran (𝑗 ∈ (𝐴 “ {(1st ‘𝑥)}) ↦ ((1st
‘𝑥)𝑆𝑗)) | 
| 239 | 238 | a1i 11 | . . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → ∀𝑖 ∈ (𝐴 “ {(1st ‘𝑥)})((1st ‘𝑥)𝑆𝑖) ∈ ran (𝑗 ∈ (𝐴 “ {(1st ‘𝑥)}) ↦ ((1st
‘𝑥)𝑆𝑗))) | 
| 240 |  | oveq1 7439 | . . . . . . . . . . . . . . . 16
⊢ (𝑦 = (1st ‘𝑥) → (𝑦𝑆𝑖) = ((1st ‘𝑥)𝑆𝑖)) | 
| 241 | 240 | eleq1d 2825 | . . . . . . . . . . . . . . 15
⊢ (𝑦 = (1st ‘𝑥) → ((𝑦𝑆𝑖) ∈ ran (𝑗 ∈ (𝐴 “ {(1st ‘𝑥)}) ↦ ((1st
‘𝑥)𝑆𝑗)) ↔ ((1st ‘𝑥)𝑆𝑖) ∈ ran (𝑗 ∈ (𝐴 “ {(1st ‘𝑥)}) ↦ ((1st
‘𝑥)𝑆𝑗)))) | 
| 242 | 241 | ralbidv 3177 | . . . . . . . . . . . . . 14
⊢ (𝑦 = (1st ‘𝑥) → (∀𝑖 ∈ (𝐴 “ {(1st ‘𝑥)})(𝑦𝑆𝑖) ∈ ran (𝑗 ∈ (𝐴 “ {(1st ‘𝑥)}) ↦ ((1st
‘𝑥)𝑆𝑗)) ↔ ∀𝑖 ∈ (𝐴 “ {(1st ‘𝑥)})((1st ‘𝑥)𝑆𝑖) ∈ ran (𝑗 ∈ (𝐴 “ {(1st ‘𝑥)}) ↦ ((1st
‘𝑥)𝑆𝑗)))) | 
| 243 | 91, 242 | ralsn 4680 | . . . . . . . . . . . . 13
⊢
(∀𝑦 ∈
{(1st ‘𝑥)}∀𝑖 ∈ (𝐴 “ {(1st ‘𝑥)})(𝑦𝑆𝑖) ∈ ran (𝑗 ∈ (𝐴 “ {(1st ‘𝑥)}) ↦ ((1st
‘𝑥)𝑆𝑗)) ↔ ∀𝑖 ∈ (𝐴 “ {(1st ‘𝑥)})((1st ‘𝑥)𝑆𝑖) ∈ ran (𝑗 ∈ (𝐴 “ {(1st ‘𝑥)}) ↦ ((1st
‘𝑥)𝑆𝑗))) | 
| 244 | 239, 243 | sylibr 234 | . . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → ∀𝑦 ∈ {(1st ‘𝑥)}∀𝑖 ∈ (𝐴 “ {(1st ‘𝑥)})(𝑦𝑆𝑖) ∈ ran (𝑗 ∈ (𝐴 “ {(1st ‘𝑥)}) ↦ ((1st
‘𝑥)𝑆𝑗))) | 
| 245 | 41 | adantr 480 | . . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝑆:𝐴⟶(SubGrp‘𝐺)) | 
| 246 | 245 | ffund 6739 | . . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → Fun 𝑆) | 
| 247 |  | resss 6018 | . . . . . . . . . . . . . . 15
⊢ (𝐴 ↾ {(1st
‘𝑥)}) ⊆ 𝐴 | 
| 248 | 230, 247 | eqsstrri 4030 | . . . . . . . . . . . . . 14
⊢
({(1st ‘𝑥)} × (𝐴 “ {(1st ‘𝑥)})) ⊆ 𝐴 | 
| 249 | 245 | fdmd 6745 | . . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → dom 𝑆 = 𝐴) | 
| 250 | 248, 249 | sseqtrrid 4026 | . . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → ({(1st ‘𝑥)} × (𝐴 “ {(1st ‘𝑥)})) ⊆ dom 𝑆) | 
| 251 |  | funimassov 7611 | . . . . . . . . . . . . 13
⊢ ((Fun
𝑆 ∧ ({(1st
‘𝑥)} × (𝐴 “ {(1st
‘𝑥)})) ⊆ dom
𝑆) → ((𝑆 “ ({(1st
‘𝑥)} × (𝐴 “ {(1st
‘𝑥)}))) ⊆ ran
(𝑗 ∈ (𝐴 “ {(1st
‘𝑥)}) ↦
((1st ‘𝑥)𝑆𝑗)) ↔ ∀𝑦 ∈ {(1st ‘𝑥)}∀𝑖 ∈ (𝐴 “ {(1st ‘𝑥)})(𝑦𝑆𝑖) ∈ ran (𝑗 ∈ (𝐴 “ {(1st ‘𝑥)}) ↦ ((1st
‘𝑥)𝑆𝑗)))) | 
| 252 | 246, 250,
251 | syl2anc 584 | . . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → ((𝑆 “ ({(1st ‘𝑥)} × (𝐴 “ {(1st ‘𝑥)}))) ⊆ ran (𝑗 ∈ (𝐴 “ {(1st ‘𝑥)}) ↦ ((1st
‘𝑥)𝑆𝑗)) ↔ ∀𝑦 ∈ {(1st ‘𝑥)}∀𝑖 ∈ (𝐴 “ {(1st ‘𝑥)})(𝑦𝑆𝑖) ∈ ran (𝑗 ∈ (𝐴 “ {(1st ‘𝑥)}) ↦ ((1st
‘𝑥)𝑆𝑗)))) | 
| 253 | 244, 252 | mpbird 257 | . . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝑆 “ ({(1st ‘𝑥)} × (𝐴 “ {(1st ‘𝑥)}))) ⊆ ran (𝑗 ∈ (𝐴 “ {(1st ‘𝑥)}) ↦ ((1st
‘𝑥)𝑆𝑗))) | 
| 254 | 233, 253 | sstrid 3994 | . . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝑆 “ ((𝐴 ↾ {(1st ‘𝑥)}) ∖ {𝑥})) ⊆ ran (𝑗 ∈ (𝐴 “ {(1st ‘𝑥)}) ↦ ((1st
‘𝑥)𝑆𝑗))) | 
| 255 | 254 | unissd 4916 | . . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → ∪ (𝑆 “ ((𝐴 ↾ {(1st ‘𝑥)}) ∖ {𝑥})) ⊆ ∪ ran
(𝑗 ∈ (𝐴 “ {(1st
‘𝑥)}) ↦
((1st ‘𝑥)𝑆𝑗))) | 
| 256 |  | df-ov 7435 | . . . . . . . . . . . . . 14
⊢
((1st ‘𝑥)𝑆𝑗) = (𝑆‘〈(1st ‘𝑥), 𝑗〉) | 
| 257 | 41 | ad2antrr 726 | . . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝑗 ∈ (𝐴 “ {(1st ‘𝑥)})) → 𝑆:𝐴⟶(SubGrp‘𝐺)) | 
| 258 |  | elrelimasn 6103 | . . . . . . . . . . . . . . . . . 18
⊢ (Rel
𝐴 → (𝑗 ∈ (𝐴 “ {(1st ‘𝑥)}) ↔ (1st
‘𝑥)𝐴𝑗)) | 
| 259 | 66, 258 | syl 17 | . . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝑗 ∈ (𝐴 “ {(1st ‘𝑥)}) ↔ (1st
‘𝑥)𝐴𝑗)) | 
| 260 | 259 | biimpa 476 | . . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝑗 ∈ (𝐴 “ {(1st ‘𝑥)})) → (1st
‘𝑥)𝐴𝑗) | 
| 261 |  | df-br 5143 | . . . . . . . . . . . . . . . 16
⊢
((1st ‘𝑥)𝐴𝑗 ↔ 〈(1st ‘𝑥), 𝑗〉 ∈ 𝐴) | 
| 262 | 260, 261 | sylib 218 | . . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝑗 ∈ (𝐴 “ {(1st ‘𝑥)})) →
〈(1st ‘𝑥), 𝑗〉 ∈ 𝐴) | 
| 263 | 257, 262 | ffvelcdmd 7104 | . . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝑗 ∈ (𝐴 “ {(1st ‘𝑥)})) → (𝑆‘〈(1st ‘𝑥), 𝑗〉) ∈ (SubGrp‘𝐺)) | 
| 264 | 256, 263 | eqeltrid 2844 | . . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝑗 ∈ (𝐴 “ {(1st ‘𝑥)})) → ((1st
‘𝑥)𝑆𝑗) ∈ (SubGrp‘𝐺)) | 
| 265 | 264 | fmpttd 7134 | . . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝑗 ∈ (𝐴 “ {(1st ‘𝑥)}) ↦ ((1st
‘𝑥)𝑆𝑗)):(𝐴 “ {(1st ‘𝑥)})⟶(SubGrp‘𝐺)) | 
| 266 | 265 | frnd 6743 | . . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → ran (𝑗 ∈ (𝐴 “ {(1st ‘𝑥)}) ↦ ((1st
‘𝑥)𝑆𝑗)) ⊆ (SubGrp‘𝐺)) | 
| 267 | 266, 207 | sstrd 3993 | . . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → ran (𝑗 ∈ (𝐴 “ {(1st ‘𝑥)}) ↦ ((1st
‘𝑥)𝑆𝑗)) ⊆ 𝒫 (Base‘𝐺)) | 
| 268 |  | sspwuni 5099 | . . . . . . . . . 10
⊢ (ran
(𝑗 ∈ (𝐴 “ {(1st
‘𝑥)}) ↦
((1st ‘𝑥)𝑆𝑗)) ⊆ 𝒫 (Base‘𝐺) ↔ ∪ ran (𝑗 ∈ (𝐴 “ {(1st ‘𝑥)}) ↦ ((1st
‘𝑥)𝑆𝑗)) ⊆ (Base‘𝐺)) | 
| 269 | 267, 268 | sylib 218 | . . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → ∪ ran
(𝑗 ∈ (𝐴 “ {(1st
‘𝑥)}) ↦
((1st ‘𝑥)𝑆𝑗)) ⊆ (Base‘𝐺)) | 
| 270 | 166, 3, 255, 269 | mrcssd 17668 | . . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝐾‘∪ (𝑆 “ ((𝐴 ↾ {(1st ‘𝑥)}) ∖ {𝑥}))) ⊆ (𝐾‘∪ ran
(𝑗 ∈ (𝐴 “ {(1st
‘𝑥)}) ↦
((1st ‘𝑥)𝑆𝑗)))) | 
| 271 | 3 | dprdspan 20048 | . . . . . . . . 9
⊢ (𝐺dom DProd (𝑗 ∈ (𝐴 “ {(1st ‘𝑥)}) ↦ ((1st
‘𝑥)𝑆𝑗)) → (𝐺 DProd (𝑗 ∈ (𝐴 “ {(1st ‘𝑥)}) ↦ ((1st
‘𝑥)𝑆𝑗))) = (𝐾‘∪ ran
(𝑗 ∈ (𝐴 “ {(1st
‘𝑥)}) ↦
((1st ‘𝑥)𝑆𝑗)))) | 
| 272 | 53, 271 | syl 17 | . . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝐺 DProd (𝑗 ∈ (𝐴 “ {(1st ‘𝑥)}) ↦ ((1st
‘𝑥)𝑆𝑗))) = (𝐾‘∪ ran
(𝑗 ∈ (𝐴 “ {(1st
‘𝑥)}) ↦
((1st ‘𝑥)𝑆𝑗)))) | 
| 273 | 270, 272 | sseqtrrd 4020 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝐾‘∪ (𝑆 “ ((𝐴 ↾ {(1st ‘𝑥)}) ∖ {𝑥}))) ⊆ (𝐺 DProd (𝑗 ∈ (𝐴 “ {(1st ‘𝑥)}) ↦ ((1st
‘𝑥)𝑆𝑗)))) | 
| 274 | 16, 17 | fnmpti 6710 | . . . . . . . . . . . . 13
⊢ (𝑖 ∈ 𝐼 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗)))) Fn 𝐼 | 
| 275 |  | fnressn 7177 | . . . . . . . . . . . . 13
⊢ (((𝑖 ∈ 𝐼 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗)))) Fn 𝐼 ∧ (1st ‘𝑥) ∈ 𝐼) → ((𝑖 ∈ 𝐼 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗)))) ↾ {(1st ‘𝑥)}) = {〈(1st
‘𝑥), ((𝑖 ∈ 𝐼 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗))))‘(1st ‘𝑥))〉}) | 
| 276 | 274, 52, 275 | sylancr 587 | . . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → ((𝑖 ∈ 𝐼 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗)))) ↾ {(1st ‘𝑥)}) = {〈(1st
‘𝑥), ((𝑖 ∈ 𝐼 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗))))‘(1st ‘𝑥))〉}) | 
| 277 | 124 | opeq2d 4879 | . . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 〈(1st ‘𝑥), ((𝑖 ∈ 𝐼 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗))))‘(1st ‘𝑥))〉 = 〈(1st
‘𝑥), (𝐺 DProd (𝑗 ∈ (𝐴 “ {(1st ‘𝑥)}) ↦ ((1st
‘𝑥)𝑆𝑗)))〉) | 
| 278 | 277 | sneqd 4637 | . . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → {〈(1st ‘𝑥), ((𝑖 ∈ 𝐼 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗))))‘(1st ‘𝑥))〉} =
{〈(1st ‘𝑥), (𝐺 DProd (𝑗 ∈ (𝐴 “ {(1st ‘𝑥)}) ↦ ((1st
‘𝑥)𝑆𝑗)))〉}) | 
| 279 | 276, 278 | eqtrd 2776 | . . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → ((𝑖 ∈ 𝐼 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗)))) ↾ {(1st ‘𝑥)}) = {〈(1st
‘𝑥), (𝐺 DProd (𝑗 ∈ (𝐴 “ {(1st ‘𝑥)}) ↦ ((1st
‘𝑥)𝑆𝑗)))〉}) | 
| 280 | 279 | oveq2d 7448 | . . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝐺 DProd ((𝑖 ∈ 𝐼 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗)))) ↾ {(1st ‘𝑥)})) = (𝐺 DProd {〈(1st ‘𝑥), (𝐺 DProd (𝑗 ∈ (𝐴 “ {(1st ‘𝑥)}) ↦ ((1st
‘𝑥)𝑆𝑗)))〉})) | 
| 281 |  | dprdsubg 20045 | . . . . . . . . . . . . 13
⊢ (𝐺dom DProd (𝑗 ∈ (𝐴 “ {(1st ‘𝑥)}) ↦ ((1st
‘𝑥)𝑆𝑗)) → (𝐺 DProd (𝑗 ∈ (𝐴 “ {(1st ‘𝑥)}) ↦ ((1st
‘𝑥)𝑆𝑗))) ∈ (SubGrp‘𝐺)) | 
| 282 | 53, 281 | syl 17 | . . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝐺 DProd (𝑗 ∈ (𝐴 “ {(1st ‘𝑥)}) ↦ ((1st
‘𝑥)𝑆𝑗))) ∈ (SubGrp‘𝐺)) | 
| 283 |  | dprdsn 20057 | . . . . . . . . . . . 12
⊢
(((1st ‘𝑥) ∈ 𝐼 ∧ (𝐺 DProd (𝑗 ∈ (𝐴 “ {(1st ‘𝑥)}) ↦ ((1st
‘𝑥)𝑆𝑗))) ∈ (SubGrp‘𝐺)) → (𝐺dom DProd {〈(1st
‘𝑥), (𝐺 DProd (𝑗 ∈ (𝐴 “ {(1st ‘𝑥)}) ↦ ((1st
‘𝑥)𝑆𝑗)))〉} ∧ (𝐺 DProd {〈(1st ‘𝑥), (𝐺 DProd (𝑗 ∈ (𝐴 “ {(1st ‘𝑥)}) ↦ ((1st
‘𝑥)𝑆𝑗)))〉}) = (𝐺 DProd (𝑗 ∈ (𝐴 “ {(1st ‘𝑥)}) ↦ ((1st
‘𝑥)𝑆𝑗))))) | 
| 284 | 52, 282, 283 | syl2anc 584 | . . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝐺dom DProd {〈(1st
‘𝑥), (𝐺 DProd (𝑗 ∈ (𝐴 “ {(1st ‘𝑥)}) ↦ ((1st
‘𝑥)𝑆𝑗)))〉} ∧ (𝐺 DProd {〈(1st ‘𝑥), (𝐺 DProd (𝑗 ∈ (𝐴 “ {(1st ‘𝑥)}) ↦ ((1st
‘𝑥)𝑆𝑗)))〉}) = (𝐺 DProd (𝑗 ∈ (𝐴 “ {(1st ‘𝑥)}) ↦ ((1st
‘𝑥)𝑆𝑗))))) | 
| 285 | 284 | simprd 495 | . . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝐺 DProd {〈(1st ‘𝑥), (𝐺 DProd (𝑗 ∈ (𝐴 “ {(1st ‘𝑥)}) ↦ ((1st
‘𝑥)𝑆𝑗)))〉}) = (𝐺 DProd (𝑗 ∈ (𝐴 “ {(1st ‘𝑥)}) ↦ ((1st
‘𝑥)𝑆𝑗)))) | 
| 286 | 280, 285 | eqtrd 2776 | . . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝐺 DProd ((𝑖 ∈ 𝐼 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗)))) ↾ {(1st ‘𝑥)})) = (𝐺 DProd (𝑗 ∈ (𝐴 “ {(1st ‘𝑥)}) ↦ ((1st
‘𝑥)𝑆𝑗)))) | 
| 287 | 4 | adantr 480 | . . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐺dom DProd (𝑖 ∈ 𝐼 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗))))) | 
| 288 | 18 | a1i 11 | . . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → dom (𝑖 ∈ 𝐼 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗)))) = 𝐼) | 
| 289 |  | difss 4135 | . . . . . . . . . . 11
⊢ (𝐼 ∖ {(1st
‘𝑥)}) ⊆ 𝐼 | 
| 290 | 289 | a1i 11 | . . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝐼 ∖ {(1st ‘𝑥)}) ⊆ 𝐼) | 
| 291 |  | disjdif 4471 | . . . . . . . . . . 11
⊢
({(1st ‘𝑥)} ∩ (𝐼 ∖ {(1st ‘𝑥)})) = ∅ | 
| 292 | 291 | a1i 11 | . . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → ({(1st ‘𝑥)} ∩ (𝐼 ∖ {(1st ‘𝑥)})) = ∅) | 
| 293 | 287, 288,
169, 290, 292, 1 | dprdcntz2 20059 | . . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝐺 DProd ((𝑖 ∈ 𝐼 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗)))) ↾ {(1st ‘𝑥)})) ⊆ ((Cntz‘𝐺)‘(𝐺 DProd ((𝑖 ∈ 𝐼 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗)))) ↾ (𝐼 ∖ {(1st ‘𝑥)}))))) | 
| 294 | 286, 293 | eqsstrrd 4018 | . . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝐺 DProd (𝑗 ∈ (𝐴 “ {(1st ‘𝑥)}) ↦ ((1st
‘𝑥)𝑆𝑗))) ⊆ ((Cntz‘𝐺)‘(𝐺 DProd ((𝑖 ∈ 𝐼 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗)))) ↾ (𝐼 ∖ {(1st ‘𝑥)}))))) | 
| 295 | 29 | adantlr 715 | . . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝑖 ∈ 𝐼) → 𝐺dom DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗))) | 
| 296 | 66, 245, 49, 295, 287, 3, 290 | dprd2dlem1 20062 | . . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝐾‘∪ (𝑆 “ (𝐴 ↾ (𝐼 ∖ {(1st ‘𝑥)})))) = (𝐺 DProd (𝑖 ∈ (𝐼 ∖ {(1st ‘𝑥)}) ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗)))))) | 
| 297 |  | resmpt 6054 | . . . . . . . . . . . 12
⊢ ((𝐼 ∖ {(1st
‘𝑥)}) ⊆ 𝐼 → ((𝑖 ∈ 𝐼 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗)))) ↾ (𝐼 ∖ {(1st ‘𝑥)})) = (𝑖 ∈ (𝐼 ∖ {(1st ‘𝑥)}) ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗))))) | 
| 298 | 289, 297 | ax-mp 5 | . . . . . . . . . . 11
⊢ ((𝑖 ∈ 𝐼 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗)))) ↾ (𝐼 ∖ {(1st ‘𝑥)})) = (𝑖 ∈ (𝐼 ∖ {(1st ‘𝑥)}) ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗)))) | 
| 299 | 298 | oveq2i 7443 | . . . . . . . . . 10
⊢ (𝐺 DProd ((𝑖 ∈ 𝐼 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗)))) ↾ (𝐼 ∖ {(1st ‘𝑥)}))) = (𝐺 DProd (𝑖 ∈ (𝐼 ∖ {(1st ‘𝑥)}) ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗))))) | 
| 300 | 296, 299 | eqtr4di 2794 | . . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝐾‘∪ (𝑆 “ (𝐴 ↾ (𝐼 ∖ {(1st ‘𝑥)})))) = (𝐺 DProd ((𝑖 ∈ 𝐼 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗)))) ↾ (𝐼 ∖ {(1st ‘𝑥)})))) | 
| 301 | 300 | fveq2d 6909 | . . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → ((Cntz‘𝐺)‘(𝐾‘∪ (𝑆 “ (𝐴 ↾ (𝐼 ∖ {(1st ‘𝑥)}))))) = ((Cntz‘𝐺)‘(𝐺 DProd ((𝑖 ∈ 𝐼 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗)))) ↾ (𝐼 ∖ {(1st ‘𝑥)}))))) | 
| 302 | 294, 301 | sseqtrrd 4020 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝐺 DProd (𝑗 ∈ (𝐴 “ {(1st ‘𝑥)}) ↦ ((1st
‘𝑥)𝑆𝑗))) ⊆ ((Cntz‘𝐺)‘(𝐾‘∪ (𝑆 “ (𝐴 ↾ (𝐼 ∖ {(1st ‘𝑥)})))))) | 
| 303 | 273, 302 | sstrd 3993 | . . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝐾‘∪ (𝑆 “ ((𝐴 ↾ {(1st ‘𝑥)}) ∖ {𝑥}))) ⊆ ((Cntz‘𝐺)‘(𝐾‘∪ (𝑆 “ (𝐴 ↾ (𝐼 ∖ {(1st ‘𝑥)})))))) | 
| 304 | 225, 1 | lsmsubg 19673 | . . . . . 6
⊢ (((𝐾‘∪ (𝑆
“ ((𝐴 ↾
{(1st ‘𝑥)}) ∖ {𝑥}))) ∈ (SubGrp‘𝐺) ∧ (𝐾‘∪ (𝑆 “ (𝐴 ↾ (𝐼 ∖ {(1st ‘𝑥)})))) ∈
(SubGrp‘𝐺) ∧
(𝐾‘∪ (𝑆
“ ((𝐴 ↾
{(1st ‘𝑥)}) ∖ {𝑥}))) ⊆ ((Cntz‘𝐺)‘(𝐾‘∪ (𝑆 “ (𝐴 ↾ (𝐼 ∖ {(1st ‘𝑥)})))))) → ((𝐾‘∪ (𝑆
“ ((𝐴 ↾
{(1st ‘𝑥)}) ∖ {𝑥})))(LSSum‘𝐺)(𝐾‘∪ (𝑆 “ (𝐴 ↾ (𝐼 ∖ {(1st ‘𝑥)}))))) ∈
(SubGrp‘𝐺)) | 
| 305 | 222, 224,
303, 304 | syl3anc 1372 | . . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → ((𝐾‘∪ (𝑆 “ ((𝐴 ↾ {(1st ‘𝑥)}) ∖ {𝑥})))(LSSum‘𝐺)(𝐾‘∪ (𝑆 “ (𝐴 ↾ (𝐼 ∖ {(1st ‘𝑥)}))))) ∈
(SubGrp‘𝐺)) | 
| 306 | 3 | mrcsscl 17664 | . . . . 5
⊢
(((SubGrp‘𝐺)
∈ (Moore‘(Base‘𝐺)) ∧ ∪ (𝑆 “ (𝐴 ∖ {𝑥})) ⊆ ((𝐾‘∪ (𝑆 “ ((𝐴 ↾ {(1st ‘𝑥)}) ∖ {𝑥})))(LSSum‘𝐺)(𝐾‘∪ (𝑆 “ (𝐴 ↾ (𝐼 ∖ {(1st ‘𝑥)}))))) ∧ ((𝐾‘∪ (𝑆
“ ((𝐴 ↾
{(1st ‘𝑥)}) ∖ {𝑥})))(LSSum‘𝐺)(𝐾‘∪ (𝑆 “ (𝐴 ↾ (𝐼 ∖ {(1st ‘𝑥)}))))) ∈
(SubGrp‘𝐺)) →
(𝐾‘∪ (𝑆
“ (𝐴 ∖ {𝑥}))) ⊆ ((𝐾‘∪ (𝑆 “ ((𝐴 ↾ {(1st ‘𝑥)}) ∖ {𝑥})))(LSSum‘𝐺)(𝐾‘∪ (𝑆 “ (𝐴 ↾ (𝐼 ∖ {(1st ‘𝑥)})))))) | 
| 307 | 166, 228,
305, 306 | syl3anc 1372 | . . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝐾‘∪ (𝑆 “ (𝐴 ∖ {𝑥}))) ⊆ ((𝐾‘∪ (𝑆 “ ((𝐴 ↾ {(1st ‘𝑥)}) ∖ {𝑥})))(LSSum‘𝐺)(𝐾‘∪ (𝑆 “ (𝐴 ↾ (𝐼 ∖ {(1st ‘𝑥)})))))) | 
| 308 |  | sslin 4242 | . . . 4
⊢ ((𝐾‘∪ (𝑆
“ (𝐴 ∖ {𝑥}))) ⊆ ((𝐾‘∪ (𝑆 “ ((𝐴 ↾ {(1st ‘𝑥)}) ∖ {𝑥})))(LSSum‘𝐺)(𝐾‘∪ (𝑆 “ (𝐴 ↾ (𝐼 ∖ {(1st ‘𝑥)}))))) → ((𝑆‘𝑥) ∩ (𝐾‘∪ (𝑆 “ (𝐴 ∖ {𝑥})))) ⊆ ((𝑆‘𝑥) ∩ ((𝐾‘∪ (𝑆 “ ((𝐴 ↾ {(1st ‘𝑥)}) ∖ {𝑥})))(LSSum‘𝐺)(𝐾‘∪ (𝑆 “ (𝐴 ↾ (𝐼 ∖ {(1st ‘𝑥)}))))))) | 
| 309 | 307, 308 | syl 17 | . . 3
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → ((𝑆‘𝑥) ∩ (𝐾‘∪ (𝑆 “ (𝐴 ∖ {𝑥})))) ⊆ ((𝑆‘𝑥) ∩ ((𝐾‘∪ (𝑆 “ ((𝐴 ↾ {(1st ‘𝑥)}) ∖ {𝑥})))(LSSum‘𝐺)(𝐾‘∪ (𝑆 “ (𝐴 ↾ (𝐼 ∖ {(1st ‘𝑥)}))))))) | 
| 310 | 41 | ffvelcdmda 7103 | . . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝑆‘𝑥) ∈ (SubGrp‘𝐺)) | 
| 311 | 225 | lsmlub 19683 | . . . . . . . . . 10
⊢ (((𝐾‘∪ (𝑆
“ ((𝐴 ↾
{(1st ‘𝑥)}) ∖ {𝑥}))) ∈ (SubGrp‘𝐺) ∧ (𝑆‘𝑥) ∈ (SubGrp‘𝐺) ∧ (𝐺 DProd (𝑗 ∈ (𝐴 “ {(1st ‘𝑥)}) ↦ ((1st
‘𝑥)𝑆𝑗))) ∈ (SubGrp‘𝐺)) → (((𝐾‘∪ (𝑆 “ ((𝐴 ↾ {(1st ‘𝑥)}) ∖ {𝑥}))) ⊆ (𝐺 DProd (𝑗 ∈ (𝐴 “ {(1st ‘𝑥)}) ↦ ((1st
‘𝑥)𝑆𝑗))) ∧ (𝑆‘𝑥) ⊆ (𝐺 DProd (𝑗 ∈ (𝐴 “ {(1st ‘𝑥)}) ↦ ((1st
‘𝑥)𝑆𝑗)))) ↔ ((𝐾‘∪ (𝑆 “ ((𝐴 ↾ {(1st ‘𝑥)}) ∖ {𝑥})))(LSSum‘𝐺)(𝑆‘𝑥)) ⊆ (𝐺 DProd (𝑗 ∈ (𝐴 “ {(1st ‘𝑥)}) ↦ ((1st
‘𝑥)𝑆𝑗))))) | 
| 312 | 222, 310,
282, 311 | syl3anc 1372 | . . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (((𝐾‘∪ (𝑆 “ ((𝐴 ↾ {(1st ‘𝑥)}) ∖ {𝑥}))) ⊆ (𝐺 DProd (𝑗 ∈ (𝐴 “ {(1st ‘𝑥)}) ↦ ((1st
‘𝑥)𝑆𝑗))) ∧ (𝑆‘𝑥) ⊆ (𝐺 DProd (𝑗 ∈ (𝐴 “ {(1st ‘𝑥)}) ↦ ((1st
‘𝑥)𝑆𝑗)))) ↔ ((𝐾‘∪ (𝑆 “ ((𝐴 ↾ {(1st ‘𝑥)}) ∖ {𝑥})))(LSSum‘𝐺)(𝑆‘𝑥)) ⊆ (𝐺 DProd (𝑗 ∈ (𝐴 “ {(1st ‘𝑥)}) ↦ ((1st
‘𝑥)𝑆𝑗))))) | 
| 313 | 273, 121,
312 | mpbi2and 712 | . . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → ((𝐾‘∪ (𝑆 “ ((𝐴 ↾ {(1st ‘𝑥)}) ∖ {𝑥})))(LSSum‘𝐺)(𝑆‘𝑥)) ⊆ (𝐺 DProd (𝑗 ∈ (𝐴 “ {(1st ‘𝑥)}) ↦ ((1st
‘𝑥)𝑆𝑗)))) | 
| 314 | 313, 124 | sseqtrrd 4020 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → ((𝐾‘∪ (𝑆 “ ((𝐴 ↾ {(1st ‘𝑥)}) ∖ {𝑥})))(LSSum‘𝐺)(𝑆‘𝑥)) ⊆ ((𝑖 ∈ 𝐼 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗))))‘(1st ‘𝑥))) | 
| 315 | 287, 288,
290 | dprdres 20049 | . . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝐺dom DProd ((𝑖 ∈ 𝐼 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗)))) ↾ (𝐼 ∖ {(1st ‘𝑥)})) ∧ (𝐺 DProd ((𝑖 ∈ 𝐼 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗)))) ↾ (𝐼 ∖ {(1st ‘𝑥)}))) ⊆ (𝐺 DProd (𝑖 ∈ 𝐼 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗))))))) | 
| 316 | 315 | simpld 494 | . . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐺dom DProd ((𝑖 ∈ 𝐼 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗)))) ↾ (𝐼 ∖ {(1st ‘𝑥)}))) | 
| 317 | 3 | dprdspan 20048 | . . . . . . . . . . 11
⊢ (𝐺dom DProd ((𝑖 ∈ 𝐼 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗)))) ↾ (𝐼 ∖ {(1st ‘𝑥)})) → (𝐺 DProd ((𝑖 ∈ 𝐼 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗)))) ↾ (𝐼 ∖ {(1st ‘𝑥)}))) = (𝐾‘∪ ran
((𝑖 ∈ 𝐼 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗)))) ↾ (𝐼 ∖ {(1st ‘𝑥)})))) | 
| 318 | 316, 317 | syl 17 | . . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝐺 DProd ((𝑖 ∈ 𝐼 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗)))) ↾ (𝐼 ∖ {(1st ‘𝑥)}))) = (𝐾‘∪ ran
((𝑖 ∈ 𝐼 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗)))) ↾ (𝐼 ∖ {(1st ‘𝑥)})))) | 
| 319 |  | df-ima 5697 | . . . . . . . . . . . 12
⊢ ((𝑖 ∈ 𝐼 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗)))) “ (𝐼 ∖ {(1st ‘𝑥)})) = ran ((𝑖 ∈ 𝐼 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗)))) ↾ (𝐼 ∖ {(1st ‘𝑥)})) | 
| 320 | 319 | unieqi 4918 | . . . . . . . . . . 11
⊢ ∪ ((𝑖
∈ 𝐼 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗)))) “ (𝐼 ∖ {(1st ‘𝑥)})) = ∪ ran ((𝑖 ∈ 𝐼 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗)))) ↾ (𝐼 ∖ {(1st ‘𝑥)})) | 
| 321 | 320 | fveq2i 6908 | . . . . . . . . . 10
⊢ (𝐾‘∪ ((𝑖
∈ 𝐼 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗)))) “ (𝐼 ∖ {(1st ‘𝑥)}))) = (𝐾‘∪ ran
((𝑖 ∈ 𝐼 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗)))) ↾ (𝐼 ∖ {(1st ‘𝑥)}))) | 
| 322 | 318, 321 | eqtr4di 2794 | . . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝐺 DProd ((𝑖 ∈ 𝐼 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗)))) ↾ (𝐼 ∖ {(1st ‘𝑥)}))) = (𝐾‘∪ ((𝑖 ∈ 𝐼 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗)))) “ (𝐼 ∖ {(1st ‘𝑥)})))) | 
| 323 | 300, 322 | eqtrd 2776 | . . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝐾‘∪ (𝑆 “ (𝐴 ↾ (𝐼 ∖ {(1st ‘𝑥)})))) = (𝐾‘∪ ((𝑖 ∈ 𝐼 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗)))) “ (𝐼 ∖ {(1st ‘𝑥)})))) | 
| 324 |  | eqimss 4041 | . . . . . . . 8
⊢ ((𝐾‘∪ (𝑆
“ (𝐴 ↾ (𝐼 ∖ {(1st
‘𝑥)})))) = (𝐾‘∪ ((𝑖
∈ 𝐼 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗)))) “ (𝐼 ∖ {(1st ‘𝑥)}))) → (𝐾‘∪ (𝑆 “ (𝐴 ↾ (𝐼 ∖ {(1st ‘𝑥)})))) ⊆ (𝐾‘∪ ((𝑖
∈ 𝐼 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗)))) “ (𝐼 ∖ {(1st ‘𝑥)})))) | 
| 325 | 323, 324 | syl 17 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝐾‘∪ (𝑆 “ (𝐴 ↾ (𝐼 ∖ {(1st ‘𝑥)})))) ⊆ (𝐾‘∪ ((𝑖
∈ 𝐼 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗)))) “ (𝐼 ∖ {(1st ‘𝑥)})))) | 
| 326 |  | ss2in 4244 | . . . . . . 7
⊢ ((((𝐾‘∪ (𝑆
“ ((𝐴 ↾
{(1st ‘𝑥)}) ∖ {𝑥})))(LSSum‘𝐺)(𝑆‘𝑥)) ⊆ ((𝑖 ∈ 𝐼 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗))))‘(1st ‘𝑥)) ∧ (𝐾‘∪ (𝑆 “ (𝐴 ↾ (𝐼 ∖ {(1st ‘𝑥)})))) ⊆ (𝐾‘∪ ((𝑖
∈ 𝐼 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗)))) “ (𝐼 ∖ {(1st ‘𝑥)})))) → (((𝐾‘∪ (𝑆
“ ((𝐴 ↾
{(1st ‘𝑥)}) ∖ {𝑥})))(LSSum‘𝐺)(𝑆‘𝑥)) ∩ (𝐾‘∪ (𝑆 “ (𝐴 ↾ (𝐼 ∖ {(1st ‘𝑥)}))))) ⊆ (((𝑖 ∈ 𝐼 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗))))‘(1st ‘𝑥)) ∩ (𝐾‘∪ ((𝑖 ∈ 𝐼 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗)))) “ (𝐼 ∖ {(1st ‘𝑥)}))))) | 
| 327 | 314, 325,
326 | syl2anc 584 | . . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (((𝐾‘∪ (𝑆 “ ((𝐴 ↾ {(1st ‘𝑥)}) ∖ {𝑥})))(LSSum‘𝐺)(𝑆‘𝑥)) ∩ (𝐾‘∪ (𝑆 “ (𝐴 ↾ (𝐼 ∖ {(1st ‘𝑥)}))))) ⊆ (((𝑖 ∈ 𝐼 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗))))‘(1st ‘𝑥)) ∩ (𝐾‘∪ ((𝑖 ∈ 𝐼 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗)))) “ (𝐼 ∖ {(1st ‘𝑥)}))))) | 
| 328 | 287, 288,
52, 2, 3 | dprddisj 20030 | . . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (((𝑖 ∈ 𝐼 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗))))‘(1st ‘𝑥)) ∩ (𝐾‘∪ ((𝑖 ∈ 𝐼 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗)))) “ (𝐼 ∖ {(1st ‘𝑥)})))) =
{(0g‘𝐺)}) | 
| 329 | 327, 328 | sseqtrd 4019 | . . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (((𝐾‘∪ (𝑆 “ ((𝐴 ↾ {(1st ‘𝑥)}) ∖ {𝑥})))(LSSum‘𝐺)(𝑆‘𝑥)) ∩ (𝐾‘∪ (𝑆 “ (𝐴 ↾ (𝐼 ∖ {(1st ‘𝑥)}))))) ⊆
{(0g‘𝐺)}) | 
| 330 | 225 | lsmub2 19677 | . . . . . . . . 9
⊢ (((𝐾‘∪ (𝑆
“ ((𝐴 ↾
{(1st ‘𝑥)}) ∖ {𝑥}))) ∈ (SubGrp‘𝐺) ∧ (𝑆‘𝑥) ∈ (SubGrp‘𝐺)) → (𝑆‘𝑥) ⊆ ((𝐾‘∪ (𝑆 “ ((𝐴 ↾ {(1st ‘𝑥)}) ∖ {𝑥})))(LSSum‘𝐺)(𝑆‘𝑥))) | 
| 331 | 222, 310,
330 | syl2anc 584 | . . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝑆‘𝑥) ⊆ ((𝐾‘∪ (𝑆 “ ((𝐴 ↾ {(1st ‘𝑥)}) ∖ {𝑥})))(LSSum‘𝐺)(𝑆‘𝑥))) | 
| 332 | 2 | subg0cl 19153 | . . . . . . . . 9
⊢ ((𝑆‘𝑥) ∈ (SubGrp‘𝐺) → (0g‘𝐺) ∈ (𝑆‘𝑥)) | 
| 333 | 310, 332 | syl 17 | . . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (0g‘𝐺) ∈ (𝑆‘𝑥)) | 
| 334 | 331, 333 | sseldd 3983 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (0g‘𝐺) ∈ ((𝐾‘∪ (𝑆 “ ((𝐴 ↾ {(1st ‘𝑥)}) ∖ {𝑥})))(LSSum‘𝐺)(𝑆‘𝑥))) | 
| 335 | 2 | subg0cl 19153 | . . . . . . . 8
⊢ ((𝐾‘∪ (𝑆
“ (𝐴 ↾ (𝐼 ∖ {(1st
‘𝑥)})))) ∈
(SubGrp‘𝐺) →
(0g‘𝐺)
∈ (𝐾‘∪ (𝑆
“ (𝐴 ↾ (𝐼 ∖ {(1st
‘𝑥)}))))) | 
| 336 | 224, 335 | syl 17 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (0g‘𝐺) ∈ (𝐾‘∪ (𝑆 “ (𝐴 ↾ (𝐼 ∖ {(1st ‘𝑥)}))))) | 
| 337 | 334, 336 | elind 4199 | . . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (0g‘𝐺) ∈ (((𝐾‘∪ (𝑆 “ ((𝐴 ↾ {(1st ‘𝑥)}) ∖ {𝑥})))(LSSum‘𝐺)(𝑆‘𝑥)) ∩ (𝐾‘∪ (𝑆 “ (𝐴 ↾ (𝐼 ∖ {(1st ‘𝑥)})))))) | 
| 338 | 337 | snssd 4808 | . . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → {(0g‘𝐺)} ⊆ (((𝐾‘∪ (𝑆 “ ((𝐴 ↾ {(1st ‘𝑥)}) ∖ {𝑥})))(LSSum‘𝐺)(𝑆‘𝑥)) ∩ (𝐾‘∪ (𝑆 “ (𝐴 ↾ (𝐼 ∖ {(1st ‘𝑥)})))))) | 
| 339 | 329, 338 | eqssd 4000 | . . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (((𝐾‘∪ (𝑆 “ ((𝐴 ↾ {(1st ‘𝑥)}) ∖ {𝑥})))(LSSum‘𝐺)(𝑆‘𝑥)) ∩ (𝐾‘∪ (𝑆 “ (𝐴 ↾ (𝐼 ∖ {(1st ‘𝑥)}))))) =
{(0g‘𝐺)}) | 
| 340 |  | incom 4208 | . . . . 5
⊢ ((𝐾‘∪ (𝑆
“ ((𝐴 ↾
{(1st ‘𝑥)}) ∖ {𝑥}))) ∩ (𝑆‘𝑥)) = ((𝑆‘𝑥) ∩ (𝐾‘∪ (𝑆 “ ((𝐴 ↾ {(1st ‘𝑥)}) ∖ {𝑥})))) | 
| 341 | 69, 101 | syl 17 | . . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → ((𝑗 ∈ (𝐴 “ {(1st ‘𝑥)}) ↦ ((1st
‘𝑥)𝑆𝑗))‘(2nd ‘𝑥)) = ((1st
‘𝑥)𝑆(2nd ‘𝑥))) | 
| 342 | 61 | fveq2d 6909 | . . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝑆‘𝑥) = (𝑆‘〈(1st ‘𝑥), (2nd ‘𝑥)〉)) | 
| 343 | 99, 341, 342 | 3eqtr4a 2802 | . . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → ((𝑗 ∈ (𝐴 “ {(1st ‘𝑥)}) ↦ ((1st
‘𝑥)𝑆𝑗))‘(2nd ‘𝑥)) = (𝑆‘𝑥)) | 
| 344 |  | eqimss2 4042 | . . . . . . . . 9
⊢ (((𝑗 ∈ (𝐴 “ {(1st ‘𝑥)}) ↦ ((1st
‘𝑥)𝑆𝑗))‘(2nd ‘𝑥)) = (𝑆‘𝑥) → (𝑆‘𝑥) ⊆ ((𝑗 ∈ (𝐴 “ {(1st ‘𝑥)}) ↦ ((1st
‘𝑥)𝑆𝑗))‘(2nd ‘𝑥))) | 
| 345 | 343, 344 | syl 17 | . . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝑆‘𝑥) ⊆ ((𝑗 ∈ (𝐴 “ {(1st ‘𝑥)}) ↦ ((1st
‘𝑥)𝑆𝑗))‘(2nd ‘𝑥))) | 
| 346 |  | eldifsn 4785 | . . . . . . . . . . . . 13
⊢ (𝑦 ∈ ((𝐴 ↾ {(1st ‘𝑥)}) ∖ {𝑥}) ↔ (𝑦 ∈ (𝐴 ↾ {(1st ‘𝑥)}) ∧ 𝑦 ≠ 𝑥)) | 
| 347 | 11 | ad2antrr 726 | . . . . . . . . . . . . . . . . . . . 20
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ (𝑦 ∈ (𝐴 ↾ {(1st ‘𝑥)}) ∧ 𝑦 ≠ 𝑥)) → Rel 𝐴) | 
| 348 |  | simprl 770 | . . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ (𝑦 ∈ (𝐴 ↾ {(1st ‘𝑥)}) ∧ 𝑦 ≠ 𝑥)) → 𝑦 ∈ (𝐴 ↾ {(1st ‘𝑥)})) | 
| 349 | 247, 348 | sselid 3980 | . . . . . . . . . . . . . . . . . . . 20
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ (𝑦 ∈ (𝐴 ↾ {(1st ‘𝑥)}) ∧ 𝑦 ≠ 𝑥)) → 𝑦 ∈ 𝐴) | 
| 350 | 347, 349,
74 | syl2anc 584 | . . . . . . . . . . . . . . . . . . 19
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ (𝑦 ∈ (𝐴 ↾ {(1st ‘𝑥)}) ∧ 𝑦 ≠ 𝑥)) → 𝑦 = 〈(1st ‘𝑦), (2nd ‘𝑦)〉) | 
| 351 | 350 | fveq2d 6909 | . . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ (𝑦 ∈ (𝐴 ↾ {(1st ‘𝑥)}) ∧ 𝑦 ≠ 𝑥)) → (𝑆‘𝑦) = (𝑆‘〈(1st ‘𝑦), (2nd ‘𝑦)〉)) | 
| 352 | 351, 109 | eqtr4di 2794 | . . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ (𝑦 ∈ (𝐴 ↾ {(1st ‘𝑥)}) ∧ 𝑦 ≠ 𝑥)) → (𝑆‘𝑦) = ((1st ‘𝑦)𝑆(2nd ‘𝑦))) | 
| 353 | 350, 348 | eqeltrrd 2841 | . . . . . . . . . . . . . . . . . . . 20
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ (𝑦 ∈ (𝐴 ↾ {(1st ‘𝑥)}) ∧ 𝑦 ≠ 𝑥)) → 〈(1st ‘𝑦), (2nd ‘𝑦)〉 ∈ (𝐴 ↾ {(1st
‘𝑥)})) | 
| 354 |  | fvex 6918 | . . . . . . . . . . . . . . . . . . . . . 22
⊢
(2nd ‘𝑦) ∈ V | 
| 355 | 354 | opelresi 6004 | . . . . . . . . . . . . . . . . . . . . 21
⊢
(〈(1st ‘𝑦), (2nd ‘𝑦)〉 ∈ (𝐴 ↾ {(1st ‘𝑥)}) ↔ ((1st
‘𝑦) ∈
{(1st ‘𝑥)}
∧ 〈(1st ‘𝑦), (2nd ‘𝑦)〉 ∈ 𝐴)) | 
| 356 | 355 | simplbi 497 | . . . . . . . . . . . . . . . . . . . 20
⊢
(〈(1st ‘𝑦), (2nd ‘𝑦)〉 ∈ (𝐴 ↾ {(1st ‘𝑥)}) → (1st
‘𝑦) ∈
{(1st ‘𝑥)}) | 
| 357 | 353, 356 | syl 17 | . . . . . . . . . . . . . . . . . . 19
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ (𝑦 ∈ (𝐴 ↾ {(1st ‘𝑥)}) ∧ 𝑦 ≠ 𝑥)) → (1st ‘𝑦) ∈ {(1st
‘𝑥)}) | 
| 358 |  | elsni 4642 | . . . . . . . . . . . . . . . . . . 19
⊢
((1st ‘𝑦) ∈ {(1st ‘𝑥)} → (1st
‘𝑦) = (1st
‘𝑥)) | 
| 359 | 357, 358 | syl 17 | . . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ (𝑦 ∈ (𝐴 ↾ {(1st ‘𝑥)}) ∧ 𝑦 ≠ 𝑥)) → (1st ‘𝑦) = (1st ‘𝑥)) | 
| 360 | 359 | oveq1d 7447 | . . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ (𝑦 ∈ (𝐴 ↾ {(1st ‘𝑥)}) ∧ 𝑦 ≠ 𝑥)) → ((1st ‘𝑦)𝑆(2nd ‘𝑦)) = ((1st ‘𝑥)𝑆(2nd ‘𝑦))) | 
| 361 | 352, 360 | eqtrd 2776 | . . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ (𝑦 ∈ (𝐴 ↾ {(1st ‘𝑥)}) ∧ 𝑦 ≠ 𝑥)) → (𝑆‘𝑦) = ((1st ‘𝑥)𝑆(2nd ‘𝑦))) | 
| 362 | 348, 230 | eleqtrdi 2850 | . . . . . . . . . . . . . . . . . . 19
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ (𝑦 ∈ (𝐴 ↾ {(1st ‘𝑥)}) ∧ 𝑦 ≠ 𝑥)) → 𝑦 ∈ ({(1st ‘𝑥)} × (𝐴 “ {(1st ‘𝑥)}))) | 
| 363 |  | xp2nd 8048 | . . . . . . . . . . . . . . . . . . 19
⊢ (𝑦 ∈ ({(1st
‘𝑥)} × (𝐴 “ {(1st
‘𝑥)})) →
(2nd ‘𝑦)
∈ (𝐴 “
{(1st ‘𝑥)})) | 
| 364 | 362, 363 | syl 17 | . . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ (𝑦 ∈ (𝐴 ↾ {(1st ‘𝑥)}) ∧ 𝑦 ≠ 𝑥)) → (2nd ‘𝑦) ∈ (𝐴 “ {(1st ‘𝑥)})) | 
| 365 |  | simprr 772 | . . . . . . . . . . . . . . . . . . 19
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ (𝑦 ∈ (𝐴 ↾ {(1st ‘𝑥)}) ∧ 𝑦 ≠ 𝑥)) → 𝑦 ≠ 𝑥) | 
| 366 | 61 | adantr 480 | . . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ (𝑦 ∈ (𝐴 ↾ {(1st ‘𝑥)}) ∧ 𝑦 ≠ 𝑥)) → 𝑥 = 〈(1st ‘𝑥), (2nd ‘𝑥)〉) | 
| 367 | 350, 366 | eqeq12d 2752 | . . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ (𝑦 ∈ (𝐴 ↾ {(1st ‘𝑥)}) ∧ 𝑦 ≠ 𝑥)) → (𝑦 = 𝑥 ↔ 〈(1st ‘𝑦), (2nd ‘𝑦)〉 = 〈(1st
‘𝑥), (2nd
‘𝑥)〉)) | 
| 368 |  | fvex 6918 | . . . . . . . . . . . . . . . . . . . . . . . 24
⊢
(1st ‘𝑦) ∈ V | 
| 369 | 368, 354 | opth 5480 | . . . . . . . . . . . . . . . . . . . . . . 23
⊢
(〈(1st ‘𝑦), (2nd ‘𝑦)〉 = 〈(1st ‘𝑥), (2nd ‘𝑥)〉 ↔ ((1st
‘𝑦) = (1st
‘𝑥) ∧
(2nd ‘𝑦) =
(2nd ‘𝑥))) | 
| 370 | 369 | baib 535 | . . . . . . . . . . . . . . . . . . . . . 22
⊢
((1st ‘𝑦) = (1st ‘𝑥) → (〈(1st ‘𝑦), (2nd ‘𝑦)〉 = 〈(1st
‘𝑥), (2nd
‘𝑥)〉 ↔
(2nd ‘𝑦) =
(2nd ‘𝑥))) | 
| 371 | 359, 370 | syl 17 | . . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ (𝑦 ∈ (𝐴 ↾ {(1st ‘𝑥)}) ∧ 𝑦 ≠ 𝑥)) → (〈(1st ‘𝑦), (2nd ‘𝑦)〉 = 〈(1st
‘𝑥), (2nd
‘𝑥)〉 ↔
(2nd ‘𝑦) =
(2nd ‘𝑥))) | 
| 372 | 367, 371 | bitrd 279 | . . . . . . . . . . . . . . . . . . . 20
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ (𝑦 ∈ (𝐴 ↾ {(1st ‘𝑥)}) ∧ 𝑦 ≠ 𝑥)) → (𝑦 = 𝑥 ↔ (2nd ‘𝑦) = (2nd ‘𝑥))) | 
| 373 | 372 | necon3bid 2984 | . . . . . . . . . . . . . . . . . . 19
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ (𝑦 ∈ (𝐴 ↾ {(1st ‘𝑥)}) ∧ 𝑦 ≠ 𝑥)) → (𝑦 ≠ 𝑥 ↔ (2nd ‘𝑦) ≠ (2nd
‘𝑥))) | 
| 374 | 365, 373 | mpbid 232 | . . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ (𝑦 ∈ (𝐴 ↾ {(1st ‘𝑥)}) ∧ 𝑦 ≠ 𝑥)) → (2nd ‘𝑦) ≠ (2nd
‘𝑥)) | 
| 375 |  | eldifsn 4785 | . . . . . . . . . . . . . . . . . 18
⊢
((2nd ‘𝑦) ∈ ((𝐴 “ {(1st ‘𝑥)}) ∖ {(2nd
‘𝑥)}) ↔
((2nd ‘𝑦)
∈ (𝐴 “
{(1st ‘𝑥)}) ∧ (2nd ‘𝑦) ≠ (2nd
‘𝑥))) | 
| 376 | 364, 374,
375 | sylanbrc 583 | . . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ (𝑦 ∈ (𝐴 ↾ {(1st ‘𝑥)}) ∧ 𝑦 ≠ 𝑥)) → (2nd ‘𝑦) ∈ ((𝐴 “ {(1st ‘𝑥)}) ∖ {(2nd
‘𝑥)})) | 
| 377 |  | ovex 7465 | . . . . . . . . . . . . . . . . 17
⊢
((1st ‘𝑥)𝑆(2nd ‘𝑦)) ∈ V | 
| 378 |  | difss 4135 | . . . . . . . . . . . . . . . . . . 19
⊢ ((𝐴 “ {(1st
‘𝑥)}) ∖
{(2nd ‘𝑥)}) ⊆ (𝐴 “ {(1st ‘𝑥)}) | 
| 379 |  | resmpt 6054 | . . . . . . . . . . . . . . . . . . 19
⊢ (((𝐴 “ {(1st
‘𝑥)}) ∖
{(2nd ‘𝑥)}) ⊆ (𝐴 “ {(1st ‘𝑥)}) → ((𝑗 ∈ (𝐴 “ {(1st ‘𝑥)}) ↦ ((1st
‘𝑥)𝑆𝑗)) ↾ ((𝐴 “ {(1st ‘𝑥)}) ∖ {(2nd
‘𝑥)})) = (𝑗 ∈ ((𝐴 “ {(1st ‘𝑥)}) ∖ {(2nd
‘𝑥)}) ↦
((1st ‘𝑥)𝑆𝑗))) | 
| 380 | 378, 379 | ax-mp 5 | . . . . . . . . . . . . . . . . . 18
⊢ ((𝑗 ∈ (𝐴 “ {(1st ‘𝑥)}) ↦ ((1st
‘𝑥)𝑆𝑗)) ↾ ((𝐴 “ {(1st ‘𝑥)}) ∖ {(2nd
‘𝑥)})) = (𝑗 ∈ ((𝐴 “ {(1st ‘𝑥)}) ∖ {(2nd
‘𝑥)}) ↦
((1st ‘𝑥)𝑆𝑗)) | 
| 381 |  | oveq2 7440 | . . . . . . . . . . . . . . . . . 18
⊢ (𝑗 = (2nd ‘𝑦) → ((1st
‘𝑥)𝑆𝑗) = ((1st ‘𝑥)𝑆(2nd ‘𝑦))) | 
| 382 | 380, 381 | elrnmpt1s 5969 | . . . . . . . . . . . . . . . . 17
⊢
(((2nd ‘𝑦) ∈ ((𝐴 “ {(1st ‘𝑥)}) ∖ {(2nd
‘𝑥)}) ∧
((1st ‘𝑥)𝑆(2nd ‘𝑦)) ∈ V) → ((1st
‘𝑥)𝑆(2nd ‘𝑦)) ∈ ran ((𝑗 ∈ (𝐴 “ {(1st ‘𝑥)}) ↦ ((1st
‘𝑥)𝑆𝑗)) ↾ ((𝐴 “ {(1st ‘𝑥)}) ∖ {(2nd
‘𝑥)}))) | 
| 383 | 376, 377,
382 | sylancl 586 | . . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ (𝑦 ∈ (𝐴 ↾ {(1st ‘𝑥)}) ∧ 𝑦 ≠ 𝑥)) → ((1st ‘𝑥)𝑆(2nd ‘𝑦)) ∈ ran ((𝑗 ∈ (𝐴 “ {(1st ‘𝑥)}) ↦ ((1st
‘𝑥)𝑆𝑗)) ↾ ((𝐴 “ {(1st ‘𝑥)}) ∖ {(2nd
‘𝑥)}))) | 
| 384 | 361, 383 | eqeltrd 2840 | . . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ (𝑦 ∈ (𝐴 ↾ {(1st ‘𝑥)}) ∧ 𝑦 ≠ 𝑥)) → (𝑆‘𝑦) ∈ ran ((𝑗 ∈ (𝐴 “ {(1st ‘𝑥)}) ↦ ((1st
‘𝑥)𝑆𝑗)) ↾ ((𝐴 “ {(1st ‘𝑥)}) ∖ {(2nd
‘𝑥)}))) | 
| 385 |  | df-ima 5697 | . . . . . . . . . . . . . . 15
⊢ ((𝑗 ∈ (𝐴 “ {(1st ‘𝑥)}) ↦ ((1st
‘𝑥)𝑆𝑗)) “ ((𝐴 “ {(1st ‘𝑥)}) ∖ {(2nd
‘𝑥)})) = ran ((𝑗 ∈ (𝐴 “ {(1st ‘𝑥)}) ↦ ((1st
‘𝑥)𝑆𝑗)) ↾ ((𝐴 “ {(1st ‘𝑥)}) ∖ {(2nd
‘𝑥)})) | 
| 386 | 384, 385 | eleqtrrdi 2851 | . . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ (𝑦 ∈ (𝐴 ↾ {(1st ‘𝑥)}) ∧ 𝑦 ≠ 𝑥)) → (𝑆‘𝑦) ∈ ((𝑗 ∈ (𝐴 “ {(1st ‘𝑥)}) ↦ ((1st
‘𝑥)𝑆𝑗)) “ ((𝐴 “ {(1st ‘𝑥)}) ∖ {(2nd
‘𝑥)}))) | 
| 387 | 386 | ex 412 | . . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → ((𝑦 ∈ (𝐴 ↾ {(1st ‘𝑥)}) ∧ 𝑦 ≠ 𝑥) → (𝑆‘𝑦) ∈ ((𝑗 ∈ (𝐴 “ {(1st ‘𝑥)}) ↦ ((1st
‘𝑥)𝑆𝑗)) “ ((𝐴 “ {(1st ‘𝑥)}) ∖ {(2nd
‘𝑥)})))) | 
| 388 | 346, 387 | biimtrid 242 | . . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝑦 ∈ ((𝐴 ↾ {(1st ‘𝑥)}) ∖ {𝑥}) → (𝑆‘𝑦) ∈ ((𝑗 ∈ (𝐴 “ {(1st ‘𝑥)}) ↦ ((1st
‘𝑥)𝑆𝑗)) “ ((𝐴 “ {(1st ‘𝑥)}) ∖ {(2nd
‘𝑥)})))) | 
| 389 | 388 | ralrimiv 3144 | . . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → ∀𝑦 ∈ ((𝐴 ↾ {(1st ‘𝑥)}) ∖ {𝑥})(𝑆‘𝑦) ∈ ((𝑗 ∈ (𝐴 “ {(1st ‘𝑥)}) ↦ ((1st
‘𝑥)𝑆𝑗)) “ ((𝐴 “ {(1st ‘𝑥)}) ∖ {(2nd
‘𝑥)}))) | 
| 390 | 231, 250 | sstrid 3994 | . . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → ((𝐴 ↾ {(1st ‘𝑥)}) ∖ {𝑥}) ⊆ dom 𝑆) | 
| 391 |  | funimass4 6972 | . . . . . . . . . . . 12
⊢ ((Fun
𝑆 ∧ ((𝐴 ↾ {(1st ‘𝑥)}) ∖ {𝑥}) ⊆ dom 𝑆) → ((𝑆 “ ((𝐴 ↾ {(1st ‘𝑥)}) ∖ {𝑥})) ⊆ ((𝑗 ∈ (𝐴 “ {(1st ‘𝑥)}) ↦ ((1st
‘𝑥)𝑆𝑗)) “ ((𝐴 “ {(1st ‘𝑥)}) ∖ {(2nd
‘𝑥)})) ↔
∀𝑦 ∈ ((𝐴 ↾ {(1st
‘𝑥)}) ∖ {𝑥})(𝑆‘𝑦) ∈ ((𝑗 ∈ (𝐴 “ {(1st ‘𝑥)}) ↦ ((1st
‘𝑥)𝑆𝑗)) “ ((𝐴 “ {(1st ‘𝑥)}) ∖ {(2nd
‘𝑥)})))) | 
| 392 | 246, 390,
391 | syl2anc 584 | . . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → ((𝑆 “ ((𝐴 ↾ {(1st ‘𝑥)}) ∖ {𝑥})) ⊆ ((𝑗 ∈ (𝐴 “ {(1st ‘𝑥)}) ↦ ((1st
‘𝑥)𝑆𝑗)) “ ((𝐴 “ {(1st ‘𝑥)}) ∖ {(2nd
‘𝑥)})) ↔
∀𝑦 ∈ ((𝐴 ↾ {(1st
‘𝑥)}) ∖ {𝑥})(𝑆‘𝑦) ∈ ((𝑗 ∈ (𝐴 “ {(1st ‘𝑥)}) ↦ ((1st
‘𝑥)𝑆𝑗)) “ ((𝐴 “ {(1st ‘𝑥)}) ∖ {(2nd
‘𝑥)})))) | 
| 393 | 389, 392 | mpbird 257 | . . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝑆 “ ((𝐴 ↾ {(1st ‘𝑥)}) ∖ {𝑥})) ⊆ ((𝑗 ∈ (𝐴 “ {(1st ‘𝑥)}) ↦ ((1st
‘𝑥)𝑆𝑗)) “ ((𝐴 “ {(1st ‘𝑥)}) ∖ {(2nd
‘𝑥)}))) | 
| 394 | 393 | unissd 4916 | . . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → ∪ (𝑆 “ ((𝐴 ↾ {(1st ‘𝑥)}) ∖ {𝑥})) ⊆ ∪
((𝑗 ∈ (𝐴 “ {(1st
‘𝑥)}) ↦
((1st ‘𝑥)𝑆𝑗)) “ ((𝐴 “ {(1st ‘𝑥)}) ∖ {(2nd
‘𝑥)}))) | 
| 395 |  | imassrn 6088 | . . . . . . . . . . 11
⊢ ((𝑗 ∈ (𝐴 “ {(1st ‘𝑥)}) ↦ ((1st
‘𝑥)𝑆𝑗)) “ ((𝐴 “ {(1st ‘𝑥)}) ∖ {(2nd
‘𝑥)})) ⊆ ran
(𝑗 ∈ (𝐴 “ {(1st
‘𝑥)}) ↦
((1st ‘𝑥)𝑆𝑗)) | 
| 396 | 395, 267 | sstrid 3994 | . . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → ((𝑗 ∈ (𝐴 “ {(1st ‘𝑥)}) ↦ ((1st
‘𝑥)𝑆𝑗)) “ ((𝐴 “ {(1st ‘𝑥)}) ∖ {(2nd
‘𝑥)})) ⊆
𝒫 (Base‘𝐺)) | 
| 397 |  | sspwuni 5099 | . . . . . . . . . 10
⊢ (((𝑗 ∈ (𝐴 “ {(1st ‘𝑥)}) ↦ ((1st
‘𝑥)𝑆𝑗)) “ ((𝐴 “ {(1st ‘𝑥)}) ∖ {(2nd
‘𝑥)})) ⊆
𝒫 (Base‘𝐺)
↔ ∪ ((𝑗 ∈ (𝐴 “ {(1st ‘𝑥)}) ↦ ((1st
‘𝑥)𝑆𝑗)) “ ((𝐴 “ {(1st ‘𝑥)}) ∖ {(2nd
‘𝑥)})) ⊆
(Base‘𝐺)) | 
| 398 | 396, 397 | sylib 218 | . . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → ∪
((𝑗 ∈ (𝐴 “ {(1st
‘𝑥)}) ↦
((1st ‘𝑥)𝑆𝑗)) “ ((𝐴 “ {(1st ‘𝑥)}) ∖ {(2nd
‘𝑥)})) ⊆
(Base‘𝐺)) | 
| 399 | 166, 3, 394, 398 | mrcssd 17668 | . . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝐾‘∪ (𝑆 “ ((𝐴 ↾ {(1st ‘𝑥)}) ∖ {𝑥}))) ⊆ (𝐾‘∪ ((𝑗 ∈ (𝐴 “ {(1st ‘𝑥)}) ↦ ((1st
‘𝑥)𝑆𝑗)) “ ((𝐴 “ {(1st ‘𝑥)}) ∖ {(2nd
‘𝑥)})))) | 
| 400 |  | ss2in 4244 | . . . . . . . 8
⊢ (((𝑆‘𝑥) ⊆ ((𝑗 ∈ (𝐴 “ {(1st ‘𝑥)}) ↦ ((1st
‘𝑥)𝑆𝑗))‘(2nd ‘𝑥)) ∧ (𝐾‘∪ (𝑆 “ ((𝐴 ↾ {(1st ‘𝑥)}) ∖ {𝑥}))) ⊆ (𝐾‘∪ ((𝑗 ∈ (𝐴 “ {(1st ‘𝑥)}) ↦ ((1st
‘𝑥)𝑆𝑗)) “ ((𝐴 “ {(1st ‘𝑥)}) ∖ {(2nd
‘𝑥)})))) →
((𝑆‘𝑥) ∩ (𝐾‘∪ (𝑆 “ ((𝐴 ↾ {(1st ‘𝑥)}) ∖ {𝑥})))) ⊆ (((𝑗 ∈ (𝐴 “ {(1st ‘𝑥)}) ↦ ((1st
‘𝑥)𝑆𝑗))‘(2nd ‘𝑥)) ∩ (𝐾‘∪ ((𝑗 ∈ (𝐴 “ {(1st ‘𝑥)}) ↦ ((1st
‘𝑥)𝑆𝑗)) “ ((𝐴 “ {(1st ‘𝑥)}) ∖ {(2nd
‘𝑥)}))))) | 
| 401 | 345, 399,
400 | syl2anc 584 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → ((𝑆‘𝑥) ∩ (𝐾‘∪ (𝑆 “ ((𝐴 ↾ {(1st ‘𝑥)}) ∖ {𝑥})))) ⊆ (((𝑗 ∈ (𝐴 “ {(1st ‘𝑥)}) ↦ ((1st
‘𝑥)𝑆𝑗))‘(2nd ‘𝑥)) ∩ (𝐾‘∪ ((𝑗 ∈ (𝐴 “ {(1st ‘𝑥)}) ↦ ((1st
‘𝑥)𝑆𝑗)) “ ((𝐴 “ {(1st ‘𝑥)}) ∖ {(2nd
‘𝑥)}))))) | 
| 402 | 58 | a1i 11 | . . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → dom (𝑗 ∈ (𝐴 “ {(1st ‘𝑥)}) ↦ ((1st
‘𝑥)𝑆𝑗)) = (𝐴 “ {(1st ‘𝑥)})) | 
| 403 | 53, 402, 69, 2, 3 | dprddisj 20030 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (((𝑗 ∈ (𝐴 “ {(1st ‘𝑥)}) ↦ ((1st
‘𝑥)𝑆𝑗))‘(2nd ‘𝑥)) ∩ (𝐾‘∪ ((𝑗 ∈ (𝐴 “ {(1st ‘𝑥)}) ↦ ((1st
‘𝑥)𝑆𝑗)) “ ((𝐴 “ {(1st ‘𝑥)}) ∖ {(2nd
‘𝑥)})))) =
{(0g‘𝐺)}) | 
| 404 | 401, 403 | sseqtrd 4019 | . . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → ((𝑆‘𝑥) ∩ (𝐾‘∪ (𝑆 “ ((𝐴 ↾ {(1st ‘𝑥)}) ∖ {𝑥})))) ⊆ {(0g‘𝐺)}) | 
| 405 | 2 | subg0cl 19153 | . . . . . . . . 9
⊢ ((𝐾‘∪ (𝑆
“ ((𝐴 ↾
{(1st ‘𝑥)}) ∖ {𝑥}))) ∈ (SubGrp‘𝐺) → (0g‘𝐺) ∈ (𝐾‘∪ (𝑆 “ ((𝐴 ↾ {(1st ‘𝑥)}) ∖ {𝑥})))) | 
| 406 | 222, 405 | syl 17 | . . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (0g‘𝐺) ∈ (𝐾‘∪ (𝑆 “ ((𝐴 ↾ {(1st ‘𝑥)}) ∖ {𝑥})))) | 
| 407 | 333, 406 | elind 4199 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (0g‘𝐺) ∈ ((𝑆‘𝑥) ∩ (𝐾‘∪ (𝑆 “ ((𝐴 ↾ {(1st ‘𝑥)}) ∖ {𝑥}))))) | 
| 408 | 407 | snssd 4808 | . . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → {(0g‘𝐺)} ⊆ ((𝑆‘𝑥) ∩ (𝐾‘∪ (𝑆 “ ((𝐴 ↾ {(1st ‘𝑥)}) ∖ {𝑥}))))) | 
| 409 | 404, 408 | eqssd 4000 | . . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → ((𝑆‘𝑥) ∩ (𝐾‘∪ (𝑆 “ ((𝐴 ↾ {(1st ‘𝑥)}) ∖ {𝑥})))) = {(0g‘𝐺)}) | 
| 410 | 340, 409 | eqtrid 2788 | . . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → ((𝐾‘∪ (𝑆 “ ((𝐴 ↾ {(1st ‘𝑥)}) ∖ {𝑥}))) ∩ (𝑆‘𝑥)) = {(0g‘𝐺)}) | 
| 411 | 225, 222,
310, 224, 2, 339, 410 | lsmdisj2 19701 | . . 3
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → ((𝑆‘𝑥) ∩ ((𝐾‘∪ (𝑆 “ ((𝐴 ↾ {(1st ‘𝑥)}) ∖ {𝑥})))(LSSum‘𝐺)(𝐾‘∪ (𝑆 “ (𝐴 ↾ (𝐼 ∖ {(1st ‘𝑥)})))))) =
{(0g‘𝐺)}) | 
| 412 | 309, 411 | sseqtrd 4019 | . 2
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → ((𝑆‘𝑥) ∩ (𝐾‘∪ (𝑆 “ (𝐴 ∖ {𝑥})))) ⊆ {(0g‘𝐺)}) | 
| 413 | 1, 2, 3, 6, 40, 41, 162, 412 | dmdprdd 20020 | 1
⊢ (𝜑 → 𝐺dom DProd 𝑆) |