MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  dmdprdsplit2lem Structured version   Visualization version   GIF version

Theorem dmdprdsplit2lem 18652
Description: Lemma for dmdprdsplit 18654. (Contributed by Mario Carneiro, 26-Apr-2016.)
Hypotheses
Ref Expression
dprdsplit.2 (𝜑𝑆:𝐼⟶(SubGrp‘𝐺))
dprdsplit.i (𝜑 → (𝐶𝐷) = ∅)
dprdsplit.u (𝜑𝐼 = (𝐶𝐷))
dmdprdsplit.z 𝑍 = (Cntz‘𝐺)
dmdprdsplit.0 0 = (0g𝐺)
dmdprdsplit2.1 (𝜑𝐺dom DProd (𝑆𝐶))
dmdprdsplit2.2 (𝜑𝐺dom DProd (𝑆𝐷))
dmdprdsplit2.3 (𝜑 → (𝐺 DProd (𝑆𝐶)) ⊆ (𝑍‘(𝐺 DProd (𝑆𝐷))))
dmdprdsplit2.4 (𝜑 → ((𝐺 DProd (𝑆𝐶)) ∩ (𝐺 DProd (𝑆𝐷))) = { 0 })
dmdprdsplit2lem.k 𝐾 = (mrCls‘(SubGrp‘𝐺))
Assertion
Ref Expression
dmdprdsplit2lem ((𝜑𝑋𝐶) → ((𝑌𝐼 → (𝑋𝑌 → (𝑆𝑋) ⊆ (𝑍‘(𝑆𝑌)))) ∧ ((𝑆𝑋) ∩ (𝐾 (𝑆 “ (𝐼 ∖ {𝑋})))) ⊆ { 0 }))

Proof of Theorem dmdprdsplit2lem
Dummy variable 𝑦 is distinct from all other variables.
StepHypRef Expression
1 dprdsplit.u . . . . . 6 (𝜑𝐼 = (𝐶𝐷))
21adantr 466 . . . . 5 ((𝜑𝑋𝐶) → 𝐼 = (𝐶𝐷))
32eleq2d 2836 . . . 4 ((𝜑𝑋𝐶) → (𝑌𝐼𝑌 ∈ (𝐶𝐷)))
4 elun 3904 . . . 4 (𝑌 ∈ (𝐶𝐷) ↔ (𝑌𝐶𝑌𝐷))
53, 4syl6bb 276 . . 3 ((𝜑𝑋𝐶) → (𝑌𝐼 ↔ (𝑌𝐶𝑌𝐷)))
6 dmdprdsplit2.1 . . . . . . . 8 (𝜑𝐺dom DProd (𝑆𝐶))
76ad2antrr 705 . . . . . . 7 (((𝜑𝑋𝐶) ∧ (𝑌𝐶𝑋𝑌)) → 𝐺dom DProd (𝑆𝐶))
8 dprdsplit.2 . . . . . . . . . 10 (𝜑𝑆:𝐼⟶(SubGrp‘𝐺))
9 ssun1 3927 . . . . . . . . . . 11 𝐶 ⊆ (𝐶𝐷)
109, 1syl5sseqr 3803 . . . . . . . . . 10 (𝜑𝐶𝐼)
118, 10fssresd 6212 . . . . . . . . 9 (𝜑 → (𝑆𝐶):𝐶⟶(SubGrp‘𝐺))
1211fdmd 6193 . . . . . . . 8 (𝜑 → dom (𝑆𝐶) = 𝐶)
1312ad2antrr 705 . . . . . . 7 (((𝜑𝑋𝐶) ∧ (𝑌𝐶𝑋𝑌)) → dom (𝑆𝐶) = 𝐶)
14 simplr 752 . . . . . . 7 (((𝜑𝑋𝐶) ∧ (𝑌𝐶𝑋𝑌)) → 𝑋𝐶)
15 simprl 754 . . . . . . 7 (((𝜑𝑋𝐶) ∧ (𝑌𝐶𝑋𝑌)) → 𝑌𝐶)
16 simprr 756 . . . . . . 7 (((𝜑𝑋𝐶) ∧ (𝑌𝐶𝑋𝑌)) → 𝑋𝑌)
17 dmdprdsplit.z . . . . . . 7 𝑍 = (Cntz‘𝐺)
187, 13, 14, 15, 16, 17dprdcntz 18615 . . . . . 6 (((𝜑𝑋𝐶) ∧ (𝑌𝐶𝑋𝑌)) → ((𝑆𝐶)‘𝑋) ⊆ (𝑍‘((𝑆𝐶)‘𝑌)))
19 fvres 6350 . . . . . . 7 (𝑋𝐶 → ((𝑆𝐶)‘𝑋) = (𝑆𝑋))
2019ad2antlr 706 . . . . . 6 (((𝜑𝑋𝐶) ∧ (𝑌𝐶𝑋𝑌)) → ((𝑆𝐶)‘𝑋) = (𝑆𝑋))
21 fvres 6350 . . . . . . . 8 (𝑌𝐶 → ((𝑆𝐶)‘𝑌) = (𝑆𝑌))
2221ad2antrl 707 . . . . . . 7 (((𝜑𝑋𝐶) ∧ (𝑌𝐶𝑋𝑌)) → ((𝑆𝐶)‘𝑌) = (𝑆𝑌))
2322fveq2d 6337 . . . . . 6 (((𝜑𝑋𝐶) ∧ (𝑌𝐶𝑋𝑌)) → (𝑍‘((𝑆𝐶)‘𝑌)) = (𝑍‘(𝑆𝑌)))
2418, 20, 233sstr3d 3796 . . . . 5 (((𝜑𝑋𝐶) ∧ (𝑌𝐶𝑋𝑌)) → (𝑆𝑋) ⊆ (𝑍‘(𝑆𝑌)))
2524exp32 407 . . . 4 ((𝜑𝑋𝐶) → (𝑌𝐶 → (𝑋𝑌 → (𝑆𝑋) ⊆ (𝑍‘(𝑆𝑌)))))
2619ad2antlr 706 . . . . . . 7 (((𝜑𝑋𝐶) ∧ (𝑌𝐷𝑋𝑌)) → ((𝑆𝐶)‘𝑋) = (𝑆𝑋))
276ad2antrr 705 . . . . . . . 8 (((𝜑𝑋𝐶) ∧ (𝑌𝐷𝑋𝑌)) → 𝐺dom DProd (𝑆𝐶))
2812ad2antrr 705 . . . . . . . 8 (((𝜑𝑋𝐶) ∧ (𝑌𝐷𝑋𝑌)) → dom (𝑆𝐶) = 𝐶)
29 simplr 752 . . . . . . . 8 (((𝜑𝑋𝐶) ∧ (𝑌𝐷𝑋𝑌)) → 𝑋𝐶)
3027, 28, 29dprdub 18632 . . . . . . 7 (((𝜑𝑋𝐶) ∧ (𝑌𝐷𝑋𝑌)) → ((𝑆𝐶)‘𝑋) ⊆ (𝐺 DProd (𝑆𝐶)))
3126, 30eqsstr3d 3789 . . . . . 6 (((𝜑𝑋𝐶) ∧ (𝑌𝐷𝑋𝑌)) → (𝑆𝑋) ⊆ (𝐺 DProd (𝑆𝐶)))
32 dmdprdsplit2.3 . . . . . . . 8 (𝜑 → (𝐺 DProd (𝑆𝐶)) ⊆ (𝑍‘(𝐺 DProd (𝑆𝐷))))
3332ad2antrr 705 . . . . . . 7 (((𝜑𝑋𝐶) ∧ (𝑌𝐷𝑋𝑌)) → (𝐺 DProd (𝑆𝐶)) ⊆ (𝑍‘(𝐺 DProd (𝑆𝐷))))
34 eqid 2771 . . . . . . . . 9 (Base‘𝐺) = (Base‘𝐺)
3534dprdssv 18623 . . . . . . . 8 (𝐺 DProd (𝑆𝐷)) ⊆ (Base‘𝐺)
36 fvres 6350 . . . . . . . . . 10 (𝑌𝐷 → ((𝑆𝐷)‘𝑌) = (𝑆𝑌))
3736ad2antrl 707 . . . . . . . . 9 (((𝜑𝑋𝐶) ∧ (𝑌𝐷𝑋𝑌)) → ((𝑆𝐷)‘𝑌) = (𝑆𝑌))
38 dmdprdsplit2.2 . . . . . . . . . . 11 (𝜑𝐺dom DProd (𝑆𝐷))
3938ad2antrr 705 . . . . . . . . . 10 (((𝜑𝑋𝐶) ∧ (𝑌𝐷𝑋𝑌)) → 𝐺dom DProd (𝑆𝐷))
40 ssun2 3928 . . . . . . . . . . . . . 14 𝐷 ⊆ (𝐶𝐷)
4140, 1syl5sseqr 3803 . . . . . . . . . . . . 13 (𝜑𝐷𝐼)
428, 41fssresd 6212 . . . . . . . . . . . 12 (𝜑 → (𝑆𝐷):𝐷⟶(SubGrp‘𝐺))
4342fdmd 6193 . . . . . . . . . . 11 (𝜑 → dom (𝑆𝐷) = 𝐷)
4443ad2antrr 705 . . . . . . . . . 10 (((𝜑𝑋𝐶) ∧ (𝑌𝐷𝑋𝑌)) → dom (𝑆𝐷) = 𝐷)
45 simprl 754 . . . . . . . . . 10 (((𝜑𝑋𝐶) ∧ (𝑌𝐷𝑋𝑌)) → 𝑌𝐷)
4639, 44, 45dprdub 18632 . . . . . . . . 9 (((𝜑𝑋𝐶) ∧ (𝑌𝐷𝑋𝑌)) → ((𝑆𝐷)‘𝑌) ⊆ (𝐺 DProd (𝑆𝐷)))
4737, 46eqsstr3d 3789 . . . . . . . 8 (((𝜑𝑋𝐶) ∧ (𝑌𝐷𝑋𝑌)) → (𝑆𝑌) ⊆ (𝐺 DProd (𝑆𝐷)))
4834, 17cntz2ss 17972 . . . . . . . 8 (((𝐺 DProd (𝑆𝐷)) ⊆ (Base‘𝐺) ∧ (𝑆𝑌) ⊆ (𝐺 DProd (𝑆𝐷))) → (𝑍‘(𝐺 DProd (𝑆𝐷))) ⊆ (𝑍‘(𝑆𝑌)))
4935, 47, 48sylancr 575 . . . . . . 7 (((𝜑𝑋𝐶) ∧ (𝑌𝐷𝑋𝑌)) → (𝑍‘(𝐺 DProd (𝑆𝐷))) ⊆ (𝑍‘(𝑆𝑌)))
5033, 49sstrd 3762 . . . . . 6 (((𝜑𝑋𝐶) ∧ (𝑌𝐷𝑋𝑌)) → (𝐺 DProd (𝑆𝐶)) ⊆ (𝑍‘(𝑆𝑌)))
5131, 50sstrd 3762 . . . . 5 (((𝜑𝑋𝐶) ∧ (𝑌𝐷𝑋𝑌)) → (𝑆𝑋) ⊆ (𝑍‘(𝑆𝑌)))
5251exp32 407 . . . 4 ((𝜑𝑋𝐶) → (𝑌𝐷 → (𝑋𝑌 → (𝑆𝑋) ⊆ (𝑍‘(𝑆𝑌)))))
5325, 52jaod 848 . . 3 ((𝜑𝑋𝐶) → ((𝑌𝐶𝑌𝐷) → (𝑋𝑌 → (𝑆𝑋) ⊆ (𝑍‘(𝑆𝑌)))))
545, 53sylbid 230 . 2 ((𝜑𝑋𝐶) → (𝑌𝐼 → (𝑋𝑌 → (𝑆𝑋) ⊆ (𝑍‘(𝑆𝑌)))))
55 dprdgrp 18612 . . . . . . . 8 (𝐺dom DProd (𝑆𝐶) → 𝐺 ∈ Grp)
566, 55syl 17 . . . . . . 7 (𝜑𝐺 ∈ Grp)
5756adantr 466 . . . . . 6 ((𝜑𝑋𝐶) → 𝐺 ∈ Grp)
5834subgacs 17837 . . . . . 6 (𝐺 ∈ Grp → (SubGrp‘𝐺) ∈ (ACS‘(Base‘𝐺)))
59 acsmre 16520 . . . . . 6 ((SubGrp‘𝐺) ∈ (ACS‘(Base‘𝐺)) → (SubGrp‘𝐺) ∈ (Moore‘(Base‘𝐺)))
6057, 58, 593syl 18 . . . . 5 ((𝜑𝑋𝐶) → (SubGrp‘𝐺) ∈ (Moore‘(Base‘𝐺)))
61 difundir 4029 . . . . . . . . . . 11 ((𝐶𝐷) ∖ {𝑋}) = ((𝐶 ∖ {𝑋}) ∪ (𝐷 ∖ {𝑋}))
622difeq1d 3878 . . . . . . . . . . 11 ((𝜑𝑋𝐶) → (𝐼 ∖ {𝑋}) = ((𝐶𝐷) ∖ {𝑋}))
63 simpr 471 . . . . . . . . . . . . . . . 16 ((𝜑𝑋𝐶) → 𝑋𝐶)
6463snssd 4476 . . . . . . . . . . . . . . 15 ((𝜑𝑋𝐶) → {𝑋} ⊆ 𝐶)
65 sslin 3987 . . . . . . . . . . . . . . 15 ({𝑋} ⊆ 𝐶 → (𝐷 ∩ {𝑋}) ⊆ (𝐷𝐶))
6664, 65syl 17 . . . . . . . . . . . . . 14 ((𝜑𝑋𝐶) → (𝐷 ∩ {𝑋}) ⊆ (𝐷𝐶))
67 incom 3956 . . . . . . . . . . . . . . 15 (𝐶𝐷) = (𝐷𝐶)
68 dprdsplit.i . . . . . . . . . . . . . . . 16 (𝜑 → (𝐶𝐷) = ∅)
6968adantr 466 . . . . . . . . . . . . . . 15 ((𝜑𝑋𝐶) → (𝐶𝐷) = ∅)
7067, 69syl5eqr 2819 . . . . . . . . . . . . . 14 ((𝜑𝑋𝐶) → (𝐷𝐶) = ∅)
71 sseq0 4120 . . . . . . . . . . . . . 14 (((𝐷 ∩ {𝑋}) ⊆ (𝐷𝐶) ∧ (𝐷𝐶) = ∅) → (𝐷 ∩ {𝑋}) = ∅)
7266, 70, 71syl2anc 573 . . . . . . . . . . . . 13 ((𝜑𝑋𝐶) → (𝐷 ∩ {𝑋}) = ∅)
73 disj3 4165 . . . . . . . . . . . . 13 ((𝐷 ∩ {𝑋}) = ∅ ↔ 𝐷 = (𝐷 ∖ {𝑋}))
7472, 73sylib 208 . . . . . . . . . . . 12 ((𝜑𝑋𝐶) → 𝐷 = (𝐷 ∖ {𝑋}))
7574uneq2d 3918 . . . . . . . . . . 11 ((𝜑𝑋𝐶) → ((𝐶 ∖ {𝑋}) ∪ 𝐷) = ((𝐶 ∖ {𝑋}) ∪ (𝐷 ∖ {𝑋})))
7661, 62, 753eqtr4a 2831 . . . . . . . . . 10 ((𝜑𝑋𝐶) → (𝐼 ∖ {𝑋}) = ((𝐶 ∖ {𝑋}) ∪ 𝐷))
7776imaeq2d 5606 . . . . . . . . 9 ((𝜑𝑋𝐶) → (𝑆 “ (𝐼 ∖ {𝑋})) = (𝑆 “ ((𝐶 ∖ {𝑋}) ∪ 𝐷)))
78 imaundi 5685 . . . . . . . . 9 (𝑆 “ ((𝐶 ∖ {𝑋}) ∪ 𝐷)) = ((𝑆 “ (𝐶 ∖ {𝑋})) ∪ (𝑆𝐷))
7977, 78syl6eq 2821 . . . . . . . 8 ((𝜑𝑋𝐶) → (𝑆 “ (𝐼 ∖ {𝑋})) = ((𝑆 “ (𝐶 ∖ {𝑋})) ∪ (𝑆𝐷)))
8079unieqd 4585 . . . . . . 7 ((𝜑𝑋𝐶) → (𝑆 “ (𝐼 ∖ {𝑋})) = ((𝑆 “ (𝐶 ∖ {𝑋})) ∪ (𝑆𝐷)))
81 uniun 4594 . . . . . . 7 ((𝑆 “ (𝐶 ∖ {𝑋})) ∪ (𝑆𝐷)) = ( (𝑆 “ (𝐶 ∖ {𝑋})) ∪ (𝑆𝐷))
8280, 81syl6eq 2821 . . . . . 6 ((𝜑𝑋𝐶) → (𝑆 “ (𝐼 ∖ {𝑋})) = ( (𝑆 “ (𝐶 ∖ {𝑋})) ∪ (𝑆𝐷)))
83 dmdprdsplit2lem.k . . . . . . . . 9 𝐾 = (mrCls‘(SubGrp‘𝐺))
84 difss 3888 . . . . . . . . . . 11 (𝐶 ∖ {𝑋}) ⊆ 𝐶
85 imass2 5641 . . . . . . . . . . 11 ((𝐶 ∖ {𝑋}) ⊆ 𝐶 → (𝑆 “ (𝐶 ∖ {𝑋})) ⊆ (𝑆𝐶))
86 uniss 4596 . . . . . . . . . . 11 ((𝑆 “ (𝐶 ∖ {𝑋})) ⊆ (𝑆𝐶) → (𝑆 “ (𝐶 ∖ {𝑋})) ⊆ (𝑆𝐶))
8784, 85, 86mp2b 10 . . . . . . . . . 10 (𝑆 “ (𝐶 ∖ {𝑋})) ⊆ (𝑆𝐶)
88 imassrn 5617 . . . . . . . . . . . 12 (𝑆𝐶) ⊆ ran 𝑆
898frnd 6191 . . . . . . . . . . . . . 14 (𝜑 → ran 𝑆 ⊆ (SubGrp‘𝐺))
9089adantr 466 . . . . . . . . . . . . 13 ((𝜑𝑋𝐶) → ran 𝑆 ⊆ (SubGrp‘𝐺))
91 mresspw 16460 . . . . . . . . . . . . . 14 ((SubGrp‘𝐺) ∈ (Moore‘(Base‘𝐺)) → (SubGrp‘𝐺) ⊆ 𝒫 (Base‘𝐺))
9260, 91syl 17 . . . . . . . . . . . . 13 ((𝜑𝑋𝐶) → (SubGrp‘𝐺) ⊆ 𝒫 (Base‘𝐺))
9390, 92sstrd 3762 . . . . . . . . . . . 12 ((𝜑𝑋𝐶) → ran 𝑆 ⊆ 𝒫 (Base‘𝐺))
9488, 93syl5ss 3763 . . . . . . . . . . 11 ((𝜑𝑋𝐶) → (𝑆𝐶) ⊆ 𝒫 (Base‘𝐺))
95 sspwuni 4746 . . . . . . . . . . 11 ((𝑆𝐶) ⊆ 𝒫 (Base‘𝐺) ↔ (𝑆𝐶) ⊆ (Base‘𝐺))
9694, 95sylib 208 . . . . . . . . . 10 ((𝜑𝑋𝐶) → (𝑆𝐶) ⊆ (Base‘𝐺))
9787, 96syl5ss 3763 . . . . . . . . 9 ((𝜑𝑋𝐶) → (𝑆 “ (𝐶 ∖ {𝑋})) ⊆ (Base‘𝐺))
9860, 83, 97mrcssidd 16493 . . . . . . . 8 ((𝜑𝑋𝐶) → (𝑆 “ (𝐶 ∖ {𝑋})) ⊆ (𝐾 (𝑆 “ (𝐶 ∖ {𝑋}))))
99 imassrn 5617 . . . . . . . . . . . 12 (𝑆𝐷) ⊆ ran 𝑆
10099, 93syl5ss 3763 . . . . . . . . . . 11 ((𝜑𝑋𝐶) → (𝑆𝐷) ⊆ 𝒫 (Base‘𝐺))
101 sspwuni 4746 . . . . . . . . . . 11 ((𝑆𝐷) ⊆ 𝒫 (Base‘𝐺) ↔ (𝑆𝐷) ⊆ (Base‘𝐺))
102100, 101sylib 208 . . . . . . . . . 10 ((𝜑𝑋𝐶) → (𝑆𝐷) ⊆ (Base‘𝐺))
10360, 83, 102mrcssidd 16493 . . . . . . . . 9 ((𝜑𝑋𝐶) → (𝑆𝐷) ⊆ (𝐾 (𝑆𝐷)))
10483dprdspan 18634 . . . . . . . . . . . 12 (𝐺dom DProd (𝑆𝐷) → (𝐺 DProd (𝑆𝐷)) = (𝐾 ran (𝑆𝐷)))
10538, 104syl 17 . . . . . . . . . . 11 (𝜑 → (𝐺 DProd (𝑆𝐷)) = (𝐾 ran (𝑆𝐷)))
106 df-ima 5263 . . . . . . . . . . . . 13 (𝑆𝐷) = ran (𝑆𝐷)
107106unieqi 4584 . . . . . . . . . . . 12 (𝑆𝐷) = ran (𝑆𝐷)
108107fveq2i 6336 . . . . . . . . . . 11 (𝐾 (𝑆𝐷)) = (𝐾 ran (𝑆𝐷))
109105, 108syl6eqr 2823 . . . . . . . . . 10 (𝜑 → (𝐺 DProd (𝑆𝐷)) = (𝐾 (𝑆𝐷)))
110109adantr 466 . . . . . . . . 9 ((𝜑𝑋𝐶) → (𝐺 DProd (𝑆𝐷)) = (𝐾 (𝑆𝐷)))
111103, 110sseqtr4d 3791 . . . . . . . 8 ((𝜑𝑋𝐶) → (𝑆𝐷) ⊆ (𝐺 DProd (𝑆𝐷)))
112 unss12 3936 . . . . . . . 8 (( (𝑆 “ (𝐶 ∖ {𝑋})) ⊆ (𝐾 (𝑆 “ (𝐶 ∖ {𝑋}))) ∧ (𝑆𝐷) ⊆ (𝐺 DProd (𝑆𝐷))) → ( (𝑆 “ (𝐶 ∖ {𝑋})) ∪ (𝑆𝐷)) ⊆ ((𝐾 (𝑆 “ (𝐶 ∖ {𝑋}))) ∪ (𝐺 DProd (𝑆𝐷))))
11398, 111, 112syl2anc 573 . . . . . . 7 ((𝜑𝑋𝐶) → ( (𝑆 “ (𝐶 ∖ {𝑋})) ∪ (𝑆𝐷)) ⊆ ((𝐾 (𝑆 “ (𝐶 ∖ {𝑋}))) ∪ (𝐺 DProd (𝑆𝐷))))
11483mrccl 16479 . . . . . . . . 9 (((SubGrp‘𝐺) ∈ (Moore‘(Base‘𝐺)) ∧ (𝑆 “ (𝐶 ∖ {𝑋})) ⊆ (Base‘𝐺)) → (𝐾 (𝑆 “ (𝐶 ∖ {𝑋}))) ∈ (SubGrp‘𝐺))
11560, 97, 114syl2anc 573 . . . . . . . 8 ((𝜑𝑋𝐶) → (𝐾 (𝑆 “ (𝐶 ∖ {𝑋}))) ∈ (SubGrp‘𝐺))
116 dprdsubg 18631 . . . . . . . . . 10 (𝐺dom DProd (𝑆𝐷) → (𝐺 DProd (𝑆𝐷)) ∈ (SubGrp‘𝐺))
11738, 116syl 17 . . . . . . . . 9 (𝜑 → (𝐺 DProd (𝑆𝐷)) ∈ (SubGrp‘𝐺))
118117adantr 466 . . . . . . . 8 ((𝜑𝑋𝐶) → (𝐺 DProd (𝑆𝐷)) ∈ (SubGrp‘𝐺))
119 eqid 2771 . . . . . . . . 9 (LSSum‘𝐺) = (LSSum‘𝐺)
120119lsmunss 18280 . . . . . . . 8 (((𝐾 (𝑆 “ (𝐶 ∖ {𝑋}))) ∈ (SubGrp‘𝐺) ∧ (𝐺 DProd (𝑆𝐷)) ∈ (SubGrp‘𝐺)) → ((𝐾 (𝑆 “ (𝐶 ∖ {𝑋}))) ∪ (𝐺 DProd (𝑆𝐷))) ⊆ ((𝐾 (𝑆 “ (𝐶 ∖ {𝑋})))(LSSum‘𝐺)(𝐺 DProd (𝑆𝐷))))
121115, 118, 120syl2anc 573 . . . . . . 7 ((𝜑𝑋𝐶) → ((𝐾 (𝑆 “ (𝐶 ∖ {𝑋}))) ∪ (𝐺 DProd (𝑆𝐷))) ⊆ ((𝐾 (𝑆 “ (𝐶 ∖ {𝑋})))(LSSum‘𝐺)(𝐺 DProd (𝑆𝐷))))
122113, 121sstrd 3762 . . . . . 6 ((𝜑𝑋𝐶) → ( (𝑆 “ (𝐶 ∖ {𝑋})) ∪ (𝑆𝐷)) ⊆ ((𝐾 (𝑆 “ (𝐶 ∖ {𝑋})))(LSSum‘𝐺)(𝐺 DProd (𝑆𝐷))))
12382, 122eqsstrd 3788 . . . . 5 ((𝜑𝑋𝐶) → (𝑆 “ (𝐼 ∖ {𝑋})) ⊆ ((𝐾 (𝑆 “ (𝐶 ∖ {𝑋})))(LSSum‘𝐺)(𝐺 DProd (𝑆𝐷))))
12487a1i 11 . . . . . . . . 9 ((𝜑𝑋𝐶) → (𝑆 “ (𝐶 ∖ {𝑋})) ⊆ (𝑆𝐶))
12560, 83, 124, 96mrcssd 16492 . . . . . . . 8 ((𝜑𝑋𝐶) → (𝐾 (𝑆 “ (𝐶 ∖ {𝑋}))) ⊆ (𝐾 (𝑆𝐶)))
12683dprdspan 18634 . . . . . . . . . . 11 (𝐺dom DProd (𝑆𝐶) → (𝐺 DProd (𝑆𝐶)) = (𝐾 ran (𝑆𝐶)))
1276, 126syl 17 . . . . . . . . . 10 (𝜑 → (𝐺 DProd (𝑆𝐶)) = (𝐾 ran (𝑆𝐶)))
128 df-ima 5263 . . . . . . . . . . . 12 (𝑆𝐶) = ran (𝑆𝐶)
129128unieqi 4584 . . . . . . . . . . 11 (𝑆𝐶) = ran (𝑆𝐶)
130129fveq2i 6336 . . . . . . . . . 10 (𝐾 (𝑆𝐶)) = (𝐾 ran (𝑆𝐶))
131127, 130syl6eqr 2823 . . . . . . . . 9 (𝜑 → (𝐺 DProd (𝑆𝐶)) = (𝐾 (𝑆𝐶)))
132131adantr 466 . . . . . . . 8 ((𝜑𝑋𝐶) → (𝐺 DProd (𝑆𝐶)) = (𝐾 (𝑆𝐶)))
133125, 132sseqtr4d 3791 . . . . . . 7 ((𝜑𝑋𝐶) → (𝐾 (𝑆 “ (𝐶 ∖ {𝑋}))) ⊆ (𝐺 DProd (𝑆𝐶)))
13432adantr 466 . . . . . . 7 ((𝜑𝑋𝐶) → (𝐺 DProd (𝑆𝐶)) ⊆ (𝑍‘(𝐺 DProd (𝑆𝐷))))
135133, 134sstrd 3762 . . . . . 6 ((𝜑𝑋𝐶) → (𝐾 (𝑆 “ (𝐶 ∖ {𝑋}))) ⊆ (𝑍‘(𝐺 DProd (𝑆𝐷))))
136119, 17lsmsubg 18276 . . . . . 6 (((𝐾 (𝑆 “ (𝐶 ∖ {𝑋}))) ∈ (SubGrp‘𝐺) ∧ (𝐺 DProd (𝑆𝐷)) ∈ (SubGrp‘𝐺) ∧ (𝐾 (𝑆 “ (𝐶 ∖ {𝑋}))) ⊆ (𝑍‘(𝐺 DProd (𝑆𝐷)))) → ((𝐾 (𝑆 “ (𝐶 ∖ {𝑋})))(LSSum‘𝐺)(𝐺 DProd (𝑆𝐷))) ∈ (SubGrp‘𝐺))
137115, 118, 135, 136syl3anc 1476 . . . . 5 ((𝜑𝑋𝐶) → ((𝐾 (𝑆 “ (𝐶 ∖ {𝑋})))(LSSum‘𝐺)(𝐺 DProd (𝑆𝐷))) ∈ (SubGrp‘𝐺))
13883mrcsscl 16488 . . . . 5 (((SubGrp‘𝐺) ∈ (Moore‘(Base‘𝐺)) ∧ (𝑆 “ (𝐼 ∖ {𝑋})) ⊆ ((𝐾 (𝑆 “ (𝐶 ∖ {𝑋})))(LSSum‘𝐺)(𝐺 DProd (𝑆𝐷))) ∧ ((𝐾 (𝑆 “ (𝐶 ∖ {𝑋})))(LSSum‘𝐺)(𝐺 DProd (𝑆𝐷))) ∈ (SubGrp‘𝐺)) → (𝐾 (𝑆 “ (𝐼 ∖ {𝑋}))) ⊆ ((𝐾 (𝑆 “ (𝐶 ∖ {𝑋})))(LSSum‘𝐺)(𝐺 DProd (𝑆𝐷))))
13960, 123, 137, 138syl3anc 1476 . . . 4 ((𝜑𝑋𝐶) → (𝐾 (𝑆 “ (𝐼 ∖ {𝑋}))) ⊆ ((𝐾 (𝑆 “ (𝐶 ∖ {𝑋})))(LSSum‘𝐺)(𝐺 DProd (𝑆𝐷))))
140 sslin 3987 . . . 4 ((𝐾 (𝑆 “ (𝐼 ∖ {𝑋}))) ⊆ ((𝐾 (𝑆 “ (𝐶 ∖ {𝑋})))(LSSum‘𝐺)(𝐺 DProd (𝑆𝐷))) → ((𝑆𝑋) ∩ (𝐾 (𝑆 “ (𝐼 ∖ {𝑋})))) ⊆ ((𝑆𝑋) ∩ ((𝐾 (𝑆 “ (𝐶 ∖ {𝑋})))(LSSum‘𝐺)(𝐺 DProd (𝑆𝐷)))))
141139, 140syl 17 . . 3 ((𝜑𝑋𝐶) → ((𝑆𝑋) ∩ (𝐾 (𝑆 “ (𝐼 ∖ {𝑋})))) ⊆ ((𝑆𝑋) ∩ ((𝐾 (𝑆 “ (𝐶 ∖ {𝑋})))(LSSum‘𝐺)(𝐺 DProd (𝑆𝐷)))))
14210sselda 3752 . . . . 5 ((𝜑𝑋𝐶) → 𝑋𝐼)
1438ffvelrnda 6504 . . . . 5 ((𝜑𝑋𝐼) → (𝑆𝑋) ∈ (SubGrp‘𝐺))
144142, 143syldan 579 . . . 4 ((𝜑𝑋𝐶) → (𝑆𝑋) ∈ (SubGrp‘𝐺))
145 dmdprdsplit.0 . . . 4 0 = (0g𝐺)
14619adantl 467 . . . . . . . . 9 ((𝜑𝑋𝐶) → ((𝑆𝐶)‘𝑋) = (𝑆𝑋))
1476adantr 466 . . . . . . . . . 10 ((𝜑𝑋𝐶) → 𝐺dom DProd (𝑆𝐶))
14812adantr 466 . . . . . . . . . 10 ((𝜑𝑋𝐶) → dom (𝑆𝐶) = 𝐶)
149147, 148, 63dprdub 18632 . . . . . . . . 9 ((𝜑𝑋𝐶) → ((𝑆𝐶)‘𝑋) ⊆ (𝐺 DProd (𝑆𝐶)))
150146, 149eqsstr3d 3789 . . . . . . . 8 ((𝜑𝑋𝐶) → (𝑆𝑋) ⊆ (𝐺 DProd (𝑆𝐶)))
151 dprdsubg 18631 . . . . . . . . . . 11 (𝐺dom DProd (𝑆𝐶) → (𝐺 DProd (𝑆𝐶)) ∈ (SubGrp‘𝐺))
1526, 151syl 17 . . . . . . . . . 10 (𝜑 → (𝐺 DProd (𝑆𝐶)) ∈ (SubGrp‘𝐺))
153152adantr 466 . . . . . . . . 9 ((𝜑𝑋𝐶) → (𝐺 DProd (𝑆𝐶)) ∈ (SubGrp‘𝐺))
154119lsmlub 18285 . . . . . . . . 9 (((𝑆𝑋) ∈ (SubGrp‘𝐺) ∧ (𝐾 (𝑆 “ (𝐶 ∖ {𝑋}))) ∈ (SubGrp‘𝐺) ∧ (𝐺 DProd (𝑆𝐶)) ∈ (SubGrp‘𝐺)) → (((𝑆𝑋) ⊆ (𝐺 DProd (𝑆𝐶)) ∧ (𝐾 (𝑆 “ (𝐶 ∖ {𝑋}))) ⊆ (𝐺 DProd (𝑆𝐶))) ↔ ((𝑆𝑋)(LSSum‘𝐺)(𝐾 (𝑆 “ (𝐶 ∖ {𝑋})))) ⊆ (𝐺 DProd (𝑆𝐶))))
155144, 115, 153, 154syl3anc 1476 . . . . . . . 8 ((𝜑𝑋𝐶) → (((𝑆𝑋) ⊆ (𝐺 DProd (𝑆𝐶)) ∧ (𝐾 (𝑆 “ (𝐶 ∖ {𝑋}))) ⊆ (𝐺 DProd (𝑆𝐶))) ↔ ((𝑆𝑋)(LSSum‘𝐺)(𝐾 (𝑆 “ (𝐶 ∖ {𝑋})))) ⊆ (𝐺 DProd (𝑆𝐶))))
156150, 133, 155mpbi2and 691 . . . . . . 7 ((𝜑𝑋𝐶) → ((𝑆𝑋)(LSSum‘𝐺)(𝐾 (𝑆 “ (𝐶 ∖ {𝑋})))) ⊆ (𝐺 DProd (𝑆𝐶)))
157156ssrind 3988 . . . . . 6 ((𝜑𝑋𝐶) → (((𝑆𝑋)(LSSum‘𝐺)(𝐾 (𝑆 “ (𝐶 ∖ {𝑋})))) ∩ (𝐺 DProd (𝑆𝐷))) ⊆ ((𝐺 DProd (𝑆𝐶)) ∩ (𝐺 DProd (𝑆𝐷))))
158 dmdprdsplit2.4 . . . . . . 7 (𝜑 → ((𝐺 DProd (𝑆𝐶)) ∩ (𝐺 DProd (𝑆𝐷))) = { 0 })
159158adantr 466 . . . . . 6 ((𝜑𝑋𝐶) → ((𝐺 DProd (𝑆𝐶)) ∩ (𝐺 DProd (𝑆𝐷))) = { 0 })
160157, 159sseqtrd 3790 . . . . 5 ((𝜑𝑋𝐶) → (((𝑆𝑋)(LSSum‘𝐺)(𝐾 (𝑆 “ (𝐶 ∖ {𝑋})))) ∩ (𝐺 DProd (𝑆𝐷))) ⊆ { 0 })
161119lsmub1 18278 . . . . . . . . 9 (((𝑆𝑋) ∈ (SubGrp‘𝐺) ∧ (𝐾 (𝑆 “ (𝐶 ∖ {𝑋}))) ∈ (SubGrp‘𝐺)) → (𝑆𝑋) ⊆ ((𝑆𝑋)(LSSum‘𝐺)(𝐾 (𝑆 “ (𝐶 ∖ {𝑋})))))
162144, 115, 161syl2anc 573 . . . . . . . 8 ((𝜑𝑋𝐶) → (𝑆𝑋) ⊆ ((𝑆𝑋)(LSSum‘𝐺)(𝐾 (𝑆 “ (𝐶 ∖ {𝑋})))))
163145subg0cl 17810 . . . . . . . . 9 ((𝑆𝑋) ∈ (SubGrp‘𝐺) → 0 ∈ (𝑆𝑋))
164144, 163syl 17 . . . . . . . 8 ((𝜑𝑋𝐶) → 0 ∈ (𝑆𝑋))
165162, 164sseldd 3753 . . . . . . 7 ((𝜑𝑋𝐶) → 0 ∈ ((𝑆𝑋)(LSSum‘𝐺)(𝐾 (𝑆 “ (𝐶 ∖ {𝑋})))))
166145subg0cl 17810 . . . . . . . 8 ((𝐺 DProd (𝑆𝐷)) ∈ (SubGrp‘𝐺) → 0 ∈ (𝐺 DProd (𝑆𝐷)))
167118, 166syl 17 . . . . . . 7 ((𝜑𝑋𝐶) → 0 ∈ (𝐺 DProd (𝑆𝐷)))
168165, 167elind 3949 . . . . . 6 ((𝜑𝑋𝐶) → 0 ∈ (((𝑆𝑋)(LSSum‘𝐺)(𝐾 (𝑆 “ (𝐶 ∖ {𝑋})))) ∩ (𝐺 DProd (𝑆𝐷))))
169168snssd 4476 . . . . 5 ((𝜑𝑋𝐶) → { 0 } ⊆ (((𝑆𝑋)(LSSum‘𝐺)(𝐾 (𝑆 “ (𝐶 ∖ {𝑋})))) ∩ (𝐺 DProd (𝑆𝐷))))
170160, 169eqssd 3769 . . . 4 ((𝜑𝑋𝐶) → (((𝑆𝑋)(LSSum‘𝐺)(𝐾 (𝑆 “ (𝐶 ∖ {𝑋})))) ∩ (𝐺 DProd (𝑆𝐷))) = { 0 })
171 resima2 5572 . . . . . . . . 9 ((𝐶 ∖ {𝑋}) ⊆ 𝐶 → ((𝑆𝐶) “ (𝐶 ∖ {𝑋})) = (𝑆 “ (𝐶 ∖ {𝑋})))
17284, 171mp1i 13 . . . . . . . 8 ((𝜑𝑋𝐶) → ((𝑆𝐶) “ (𝐶 ∖ {𝑋})) = (𝑆 “ (𝐶 ∖ {𝑋})))
173172unieqd 4585 . . . . . . 7 ((𝜑𝑋𝐶) → ((𝑆𝐶) “ (𝐶 ∖ {𝑋})) = (𝑆 “ (𝐶 ∖ {𝑋})))
174173fveq2d 6337 . . . . . 6 ((𝜑𝑋𝐶) → (𝐾 ((𝑆𝐶) “ (𝐶 ∖ {𝑋}))) = (𝐾 (𝑆 “ (𝐶 ∖ {𝑋}))))
175146, 174ineq12d 3966 . . . . 5 ((𝜑𝑋𝐶) → (((𝑆𝐶)‘𝑋) ∩ (𝐾 ((𝑆𝐶) “ (𝐶 ∖ {𝑋})))) = ((𝑆𝑋) ∩ (𝐾 (𝑆 “ (𝐶 ∖ {𝑋})))))
176147, 148, 63, 145, 83dprddisj 18616 . . . . 5 ((𝜑𝑋𝐶) → (((𝑆𝐶)‘𝑋) ∩ (𝐾 ((𝑆𝐶) “ (𝐶 ∖ {𝑋})))) = { 0 })
177175, 176eqtr3d 2807 . . . 4 ((𝜑𝑋𝐶) → ((𝑆𝑋) ∩ (𝐾 (𝑆 “ (𝐶 ∖ {𝑋})))) = { 0 })
1788adantr 466 . . . . . . . 8 ((𝜑𝑋𝐶) → 𝑆:𝐼⟶(SubGrp‘𝐺))
179 ffun 6187 . . . . . . . 8 (𝑆:𝐼⟶(SubGrp‘𝐺) → Fun 𝑆)
180 funiunfv 6652 . . . . . . . 8 (Fun 𝑆 𝑦 ∈ (𝐶 ∖ {𝑋})(𝑆𝑦) = (𝑆 “ (𝐶 ∖ {𝑋})))
181178, 179, 1803syl 18 . . . . . . 7 ((𝜑𝑋𝐶) → 𝑦 ∈ (𝐶 ∖ {𝑋})(𝑆𝑦) = (𝑆 “ (𝐶 ∖ {𝑋})))
1826ad2antrr 705 . . . . . . . . . . 11 (((𝜑𝑋𝐶) ∧ 𝑦 ∈ (𝐶 ∖ {𝑋})) → 𝐺dom DProd (𝑆𝐶))
18312ad2antrr 705 . . . . . . . . . . 11 (((𝜑𝑋𝐶) ∧ 𝑦 ∈ (𝐶 ∖ {𝑋})) → dom (𝑆𝐶) = 𝐶)
184 eldifi 3883 . . . . . . . . . . . 12 (𝑦 ∈ (𝐶 ∖ {𝑋}) → 𝑦𝐶)
185184adantl 467 . . . . . . . . . . 11 (((𝜑𝑋𝐶) ∧ 𝑦 ∈ (𝐶 ∖ {𝑋})) → 𝑦𝐶)
186 simplr 752 . . . . . . . . . . 11 (((𝜑𝑋𝐶) ∧ 𝑦 ∈ (𝐶 ∖ {𝑋})) → 𝑋𝐶)
187 eldifsni 4458 . . . . . . . . . . . 12 (𝑦 ∈ (𝐶 ∖ {𝑋}) → 𝑦𝑋)
188187adantl 467 . . . . . . . . . . 11 (((𝜑𝑋𝐶) ∧ 𝑦 ∈ (𝐶 ∖ {𝑋})) → 𝑦𝑋)
189182, 183, 185, 186, 188, 17dprdcntz 18615 . . . . . . . . . 10 (((𝜑𝑋𝐶) ∧ 𝑦 ∈ (𝐶 ∖ {𝑋})) → ((𝑆𝐶)‘𝑦) ⊆ (𝑍‘((𝑆𝐶)‘𝑋)))
190 fvres 6350 . . . . . . . . . . 11 (𝑦𝐶 → ((𝑆𝐶)‘𝑦) = (𝑆𝑦))
191185, 190syl 17 . . . . . . . . . 10 (((𝜑𝑋𝐶) ∧ 𝑦 ∈ (𝐶 ∖ {𝑋})) → ((𝑆𝐶)‘𝑦) = (𝑆𝑦))
19219ad2antlr 706 . . . . . . . . . . 11 (((𝜑𝑋𝐶) ∧ 𝑦 ∈ (𝐶 ∖ {𝑋})) → ((𝑆𝐶)‘𝑋) = (𝑆𝑋))
193192fveq2d 6337 . . . . . . . . . 10 (((𝜑𝑋𝐶) ∧ 𝑦 ∈ (𝐶 ∖ {𝑋})) → (𝑍‘((𝑆𝐶)‘𝑋)) = (𝑍‘(𝑆𝑋)))
194189, 191, 1933sstr3d 3796 . . . . . . . . 9 (((𝜑𝑋𝐶) ∧ 𝑦 ∈ (𝐶 ∖ {𝑋})) → (𝑆𝑦) ⊆ (𝑍‘(𝑆𝑋)))
195194ralrimiva 3115 . . . . . . . 8 ((𝜑𝑋𝐶) → ∀𝑦 ∈ (𝐶 ∖ {𝑋})(𝑆𝑦) ⊆ (𝑍‘(𝑆𝑋)))
196 iunss 4696 . . . . . . . 8 ( 𝑦 ∈ (𝐶 ∖ {𝑋})(𝑆𝑦) ⊆ (𝑍‘(𝑆𝑋)) ↔ ∀𝑦 ∈ (𝐶 ∖ {𝑋})(𝑆𝑦) ⊆ (𝑍‘(𝑆𝑋)))
197195, 196sylibr 224 . . . . . . 7 ((𝜑𝑋𝐶) → 𝑦 ∈ (𝐶 ∖ {𝑋})(𝑆𝑦) ⊆ (𝑍‘(𝑆𝑋)))
198181, 197eqsstr3d 3789 . . . . . 6 ((𝜑𝑋𝐶) → (𝑆 “ (𝐶 ∖ {𝑋})) ⊆ (𝑍‘(𝑆𝑋)))
19934subgss 17803 . . . . . . . 8 ((𝑆𝑋) ∈ (SubGrp‘𝐺) → (𝑆𝑋) ⊆ (Base‘𝐺))
200144, 199syl 17 . . . . . . 7 ((𝜑𝑋𝐶) → (𝑆𝑋) ⊆ (Base‘𝐺))
20134, 17cntzsubg 17976 . . . . . . 7 ((𝐺 ∈ Grp ∧ (𝑆𝑋) ⊆ (Base‘𝐺)) → (𝑍‘(𝑆𝑋)) ∈ (SubGrp‘𝐺))
20257, 200, 201syl2anc 573 . . . . . 6 ((𝜑𝑋𝐶) → (𝑍‘(𝑆𝑋)) ∈ (SubGrp‘𝐺))
20383mrcsscl 16488 . . . . . 6 (((SubGrp‘𝐺) ∈ (Moore‘(Base‘𝐺)) ∧ (𝑆 “ (𝐶 ∖ {𝑋})) ⊆ (𝑍‘(𝑆𝑋)) ∧ (𝑍‘(𝑆𝑋)) ∈ (SubGrp‘𝐺)) → (𝐾 (𝑆 “ (𝐶 ∖ {𝑋}))) ⊆ (𝑍‘(𝑆𝑋)))
20460, 198, 202, 203syl3anc 1476 . . . . 5 ((𝜑𝑋𝐶) → (𝐾 (𝑆 “ (𝐶 ∖ {𝑋}))) ⊆ (𝑍‘(𝑆𝑋)))
20517, 115, 144, 204cntzrecd 18298 . . . 4 ((𝜑𝑋𝐶) → (𝑆𝑋) ⊆ (𝑍‘(𝐾 (𝑆 “ (𝐶 ∖ {𝑋})))))
206119, 144, 115, 118, 145, 170, 177, 17, 205lsmdisj3 18303 . . 3 ((𝜑𝑋𝐶) → ((𝑆𝑋) ∩ ((𝐾 (𝑆 “ (𝐶 ∖ {𝑋})))(LSSum‘𝐺)(𝐺 DProd (𝑆𝐷)))) = { 0 })
207141, 206sseqtrd 3790 . 2 ((𝜑𝑋𝐶) → ((𝑆𝑋) ∩ (𝐾 (𝑆 “ (𝐼 ∖ {𝑋})))) ⊆ { 0 })
20854, 207jca 501 1 ((𝜑𝑋𝐶) → ((𝑌𝐼 → (𝑋𝑌 → (𝑆𝑋) ⊆ (𝑍‘(𝑆𝑌)))) ∧ ((𝑆𝑋) ∩ (𝐾 (𝑆 “ (𝐼 ∖ {𝑋})))) ⊆ { 0 }))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 196  wa 382  wo 836   = wceq 1631  wcel 2145  wne 2943  wral 3061  cdif 3720  cun 3721  cin 3722  wss 3723  c0 4063  𝒫 cpw 4298  {csn 4317   cuni 4575   ciun 4655   class class class wbr 4787  dom cdm 5250  ran crn 5251  cres 5252  cima 5253  Fun wfun 6024  wf 6026  cfv 6030  (class class class)co 6796  Basecbs 16064  0gc0g 16308  Moorecmre 16450  mrClscmrc 16451  ACScacs 16453  Grpcgrp 17630  SubGrpcsubg 17796  Cntzccntz 17955  LSSumclsm 18256   DProd cdprd 18600
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1870  ax-4 1885  ax-5 1991  ax-6 2057  ax-7 2093  ax-8 2147  ax-9 2154  ax-10 2174  ax-11 2190  ax-12 2203  ax-13 2408  ax-ext 2751  ax-rep 4905  ax-sep 4916  ax-nul 4924  ax-pow 4975  ax-pr 5035  ax-un 7100  ax-inf2 8706  ax-cnex 10198  ax-resscn 10199  ax-1cn 10200  ax-icn 10201  ax-addcl 10202  ax-addrcl 10203  ax-mulcl 10204  ax-mulrcl 10205  ax-mulcom 10206  ax-addass 10207  ax-mulass 10208  ax-distr 10209  ax-i2m1 10210  ax-1ne0 10211  ax-1rid 10212  ax-rnegex 10213  ax-rrecex 10214  ax-cnre 10215  ax-pre-lttri 10216  ax-pre-lttrn 10217  ax-pre-ltadd 10218  ax-pre-mulgt0 10219
This theorem depends on definitions:  df-bi 197  df-an 383  df-or 837  df-3or 1072  df-3an 1073  df-tru 1634  df-ex 1853  df-nf 1858  df-sb 2050  df-eu 2622  df-mo 2623  df-clab 2758  df-cleq 2764  df-clel 2767  df-nfc 2902  df-ne 2944  df-nel 3047  df-ral 3066  df-rex 3067  df-reu 3068  df-rmo 3069  df-rab 3070  df-v 3353  df-sbc 3588  df-csb 3683  df-dif 3726  df-un 3728  df-in 3730  df-ss 3737  df-pss 3739  df-nul 4064  df-if 4227  df-pw 4300  df-sn 4318  df-pr 4320  df-tp 4322  df-op 4324  df-uni 4576  df-int 4613  df-iun 4657  df-iin 4658  df-br 4788  df-opab 4848  df-mpt 4865  df-tr 4888  df-id 5158  df-eprel 5163  df-po 5171  df-so 5172  df-fr 5209  df-se 5210  df-we 5211  df-xp 5256  df-rel 5257  df-cnv 5258  df-co 5259  df-dm 5260  df-rn 5261  df-res 5262  df-ima 5263  df-pred 5822  df-ord 5868  df-on 5869  df-lim 5870  df-suc 5871  df-iota 5993  df-fun 6032  df-fn 6033  df-f 6034  df-f1 6035  df-fo 6036  df-f1o 6037  df-fv 6038  df-isom 6039  df-riota 6757  df-ov 6799  df-oprab 6800  df-mpt2 6801  df-of 7048  df-om 7217  df-1st 7319  df-2nd 7320  df-supp 7451  df-tpos 7508  df-wrecs 7563  df-recs 7625  df-rdg 7663  df-1o 7717  df-oadd 7721  df-er 7900  df-map 8015  df-ixp 8067  df-en 8114  df-dom 8115  df-sdom 8116  df-fin 8117  df-fsupp 8436  df-oi 8575  df-card 8969  df-pnf 10282  df-mnf 10283  df-xr 10284  df-ltxr 10285  df-le 10286  df-sub 10474  df-neg 10475  df-nn 11227  df-2 11285  df-n0 11500  df-z 11585  df-uz 11894  df-fz 12534  df-fzo 12674  df-seq 13009  df-hash 13322  df-ndx 16067  df-slot 16068  df-base 16070  df-sets 16071  df-ress 16072  df-plusg 16162  df-0g 16310  df-gsum 16311  df-mre 16454  df-mrc 16455  df-acs 16457  df-mgm 17450  df-sgrp 17492  df-mnd 17503  df-mhm 17543  df-submnd 17544  df-grp 17633  df-minusg 17634  df-sbg 17635  df-mulg 17749  df-subg 17799  df-ghm 17866  df-gim 17909  df-cntz 17957  df-oppg 17983  df-lsm 18258  df-cmn 18402  df-dprd 18602
This theorem is referenced by:  dmdprdsplit2  18653
  Copyright terms: Public domain W3C validator