Theorem imasplusg 13689

Description: The group operation in an image structure. (Contributed by Mario Carneiro, 23-Feb-2015.) (Revised by Mario Carneiro, 11-Jul-2015.) (Revised by Thierry Arnoux, 16-Jun-2019.)

Hypotheses

Ref	Expression
imasbas.u	⊢ (𝜑 → 𝑈 = (𝐹 “s 𝑅))
imasbas.v	⊢ (𝜑 → 𝑉 = (Base‘𝑅))
imasbas.f	⊢ (𝜑 → 𝐹:𝑉–onto→𝐵)
imasbas.r	⊢ (𝜑 → 𝑅 ∈ 𝑍)
imasplusg.p	⊢ + = (+g‘𝑅)
imasplusg.a	⊢ + = (+g‘𝑈)

Assertion

Ref	Expression
imasplusg	⊢ (𝜑 → + = ∪ 𝑝 ∈ 𝑉 ∪ 𝑞 ∈ 𝑉 {⟨⟨(𝐹‘𝑝), (𝐹‘𝑞)⟩, (𝐹‘(𝑝 + 𝑞))⟩})

Distinct variable groups:   𝐹,𝑝,𝑞   𝑅,𝑝,𝑞   𝑉,𝑝,𝑞   𝜑,𝑝,𝑞

Allowed substitution hints:   𝐵(𝑞, 𝑝)   + (𝑞, 𝑝)   + (𝑞, 𝑝)   𝑈(𝑞, 𝑝)   𝑍(𝑞, 𝑝)

Proof of Theorem imasplusg

Step	Hyp	Ref	Expression
1		imasplusg.a	. . 3 ⊢ + = (+g‘𝑈)
2		imasbas.u	. . . . . 6 ⊢ (𝜑 → 𝑈 = (𝐹 “s 𝑅))
3		imasbas.v	. . . . . 6 ⊢ (𝜑 → 𝑉 = (Base‘𝑅))
4		eqid 2238	. . . . . 6 ⊢ (+g‘𝑅) = (+g‘𝑅)
5		eqid 2238	. . . . . 6 ⊢ (.r‘𝑅) = (.r‘𝑅)
6		eqid 2238	. . . . . 6 ⊢ ( ·𝑠 ‘𝑅) = ( ·𝑠 ‘𝑅)
7		eqidd 2239	. . . . . 6 ⊢ (𝜑 → ∪ 𝑝 ∈ 𝑉 ∪ 𝑞 ∈ 𝑉 {⟨⟨(𝐹‘𝑝), (𝐹‘𝑞)⟩, (𝐹‘(𝑝(+g‘𝑅)𝑞))⟩} = ∪ 𝑝 ∈ 𝑉 ∪ 𝑞 ∈ 𝑉 {⟨⟨(𝐹‘𝑝), (𝐹‘𝑞)⟩, (𝐹‘(𝑝(+g‘𝑅)𝑞))⟩})
8		eqidd 2239	. . . . . 6 ⊢ (𝜑 → ∪ 𝑝 ∈ 𝑉 ∪ 𝑞 ∈ 𝑉 {⟨⟨(𝐹‘𝑝), (𝐹‘𝑞)⟩, (𝐹‘(𝑝(.r‘𝑅)𝑞))⟩} = ∪ 𝑝 ∈ 𝑉 ∪ 𝑞 ∈ 𝑉 {⟨⟨(𝐹‘𝑝), (𝐹‘𝑞)⟩, (𝐹‘(𝑝(.r‘𝑅)𝑞))⟩})
9		imasbas.f	. . . . . 6 ⊢ (𝜑 → 𝐹:𝑉–onto→𝐵)
10		imasbas.r	. . . . . 6 ⊢ (𝜑 → 𝑅 ∈ 𝑍)
11	2, 3, 4, 5, 6, 7, 8, 9, 10	imasival 13687	. . . . 5 ⊢ (𝜑 → 𝑈 = {⟨(Base‘ndx), 𝐵⟩, ⟨(+g‘ndx), ∪ 𝑝 ∈ 𝑉 ∪ 𝑞 ∈ 𝑉 {⟨⟨(𝐹‘𝑝), (𝐹‘𝑞)⟩, (𝐹‘(𝑝(+g‘𝑅)𝑞))⟩}⟩, ⟨(.r‘ndx), ∪ 𝑝 ∈ 𝑉 ∪ 𝑞 ∈ 𝑉 {⟨⟨(𝐹‘𝑝), (𝐹‘𝑞)⟩, (𝐹‘(𝑝(.r‘𝑅)𝑞))⟩}⟩})
12	11	fveq1d 5700	. . . 4 ⊢ (𝜑 → (𝑈‘(+g‘ndx)) = ({⟨(Base‘ndx), 𝐵⟩, ⟨(+g‘ndx), ∪ 𝑝 ∈ 𝑉 ∪ 𝑞 ∈ 𝑉 {⟨⟨(𝐹‘𝑝), (𝐹‘𝑞)⟩, (𝐹‘(𝑝(+g‘𝑅)𝑞))⟩}⟩, ⟨(.r‘ndx), ∪ 𝑝 ∈ 𝑉 ∪ 𝑞 ∈ 𝑉 {⟨⟨(𝐹‘𝑝), (𝐹‘𝑞)⟩, (𝐹‘(𝑝(.r‘𝑅)𝑞))⟩}⟩}‘(+g‘ndx)))
13		basendxnn 13467	. . . . . . . 8 ⊢ (Base‘ndx) ∈ ℕ
14		basfn 13470	. . . . . . . . . . 11 ⊢ Base Fn V
15	10	elexd 2835	. . . . . . . . . . 11 ⊢ (𝜑 → 𝑅 ∈ V)
16		funfvex 5715	. . . . . . . . . . . 12 ⊢ ((Fun Base ∧ 𝑅 ∈ dom Base) → (Base‘𝑅) ∈ V)
17	16	funfni 5486	. . . . . . . . . . 11 ⊢ ((Base Fn V ∧ 𝑅 ∈ V) → (Base‘𝑅) ∈ V)
18	14, 15, 17	sylancr 418	. . . . . . . . . 10 ⊢ (𝜑 → (Base‘𝑅) ∈ V)
19	3, 18	eqeltrd 2315	. . . . . . . . 9 ⊢ (𝜑 → 𝑉 ∈ V)
20		focdmex 6348	. . . . . . . . 9 ⊢ (𝑉 ∈ V → (𝐹:𝑉–onto→𝐵 → 𝐵 ∈ V))
21	19, 9, 20	sylc 62	. . . . . . . 8 ⊢ (𝜑 → 𝐵 ∈ V)
22		opexg 4370	. . . . . . . 8 ⊢ (((Base‘ndx) ∈ ℕ ∧ 𝐵 ∈ V) → ⟨(Base‘ndx), 𝐵⟩ ∈ V)
23	13, 21, 22	sylancr 418	. . . . . . 7 ⊢ (𝜑 → ⟨(Base‘ndx), 𝐵⟩ ∈ V)
24		plusgndxnn 13525	. . . . . . . 8 ⊢ (+g‘ndx) ∈ ℕ
25		fof 5618	. . . . . . . . . . . . . . . . . 18 ⊢ (𝐹:𝑉–onto→𝐵 → 𝐹:𝑉⟶𝐵)
26	9, 25	syl 14	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → 𝐹:𝑉⟶𝐵)
27	26, 19	fexd 5951	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → 𝐹 ∈ V)
28		vex 2824	. . . . . . . . . . . . . . . 16 ⊢ 𝑝 ∈ V
29		fvexg 5717	. . . . . . . . . . . . . . . 16 ⊢ ((𝐹 ∈ V ∧ 𝑝 ∈ V) → (𝐹‘𝑝) ∈ V)
30	27, 28, 29	sylancl 417	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (𝐹‘𝑝) ∈ V)
31		vex 2824	. . . . . . . . . . . . . . . 16 ⊢ 𝑞 ∈ V
32		fvexg 5717	. . . . . . . . . . . . . . . 16 ⊢ ((𝐹 ∈ V ∧ 𝑞 ∈ V) → (𝐹‘𝑞) ∈ V)
33	27, 31, 32	sylancl 417	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (𝐹‘𝑞) ∈ V)
34		opexg 4370	. . . . . . . . . . . . . . 15 ⊢ (((𝐹‘𝑝) ∈ V ∧ (𝐹‘𝑞) ∈ V) → ⟨(𝐹‘𝑝), (𝐹‘𝑞)⟩ ∈ V)
35	30, 33, 34	syl2anc 415	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ⟨(𝐹‘𝑝), (𝐹‘𝑞)⟩ ∈ V)
36	28	a1i 9	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → 𝑝 ∈ V)
37		plusgslid 13526	. . . . . . . . . . . . . . . . . 18 ⊢ (+g = Slot (+g‘ndx) ∧ (+g‘ndx) ∈ ℕ)
38	37	slotex 13438	. . . . . . . . . . . . . . . . 17 ⊢ (𝑅 ∈ 𝑍 → (+g‘𝑅) ∈ V)
39	10, 38	syl 14	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (+g‘𝑅) ∈ V)
40	31	a1i 9	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → 𝑞 ∈ V)
41		ovexg 6122	. . . . . . . . . . . . . . . 16 ⊢ ((𝑝 ∈ V ∧ (+g‘𝑅) ∈ V ∧ 𝑞 ∈ V) → (𝑝(+g‘𝑅)𝑞) ∈ V)
42	36, 39, 40, 41	syl3anc 1278	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (𝑝(+g‘𝑅)𝑞) ∈ V)
43		fvexg 5717	. . . . . . . . . . . . . . 15 ⊢ ((𝐹 ∈ V ∧ (𝑝(+g‘𝑅)𝑞) ∈ V) → (𝐹‘(𝑝(+g‘𝑅)𝑞)) ∈ V)
44	27, 42, 43	syl2anc 415	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝐹‘(𝑝(+g‘𝑅)𝑞)) ∈ V)
45		opexg 4370	. . . . . . . . . . . . . 14 ⊢ ((⟨(𝐹‘𝑝), (𝐹‘𝑞)⟩ ∈ V ∧ (𝐹‘(𝑝(+g‘𝑅)𝑞)) ∈ V) → ⟨⟨(𝐹‘𝑝), (𝐹‘𝑞)⟩, (𝐹‘(𝑝(+g‘𝑅)𝑞))⟩ ∈ V)
46	35, 44, 45	syl2anc 415	. . . . . . . . . . . . 13 ⊢ (𝜑 → ⟨⟨(𝐹‘𝑝), (𝐹‘𝑞)⟩, (𝐹‘(𝑝(+g‘𝑅)𝑞))⟩ ∈ V)
47		snexg 4323	. . . . . . . . . . . . 13 ⊢ (⟨⟨(𝐹‘𝑝), (𝐹‘𝑞)⟩, (𝐹‘(𝑝(+g‘𝑅)𝑞))⟩ ∈ V → {⟨⟨(𝐹‘𝑝), (𝐹‘𝑞)⟩, (𝐹‘(𝑝(+g‘𝑅)𝑞))⟩} ∈ V)
48	46, 47	syl 14	. . . . . . . . . . . 12 ⊢ (𝜑 → {⟨⟨(𝐹‘𝑝), (𝐹‘𝑞)⟩, (𝐹‘(𝑝(+g‘𝑅)𝑞))⟩} ∈ V)
49	48	ralrimivw 2624	. . . . . . . . . . 11 ⊢ (𝜑 → ∀𝑞 ∈ 𝑉 {⟨⟨(𝐹‘𝑝), (𝐹‘𝑞)⟩, (𝐹‘(𝑝(+g‘𝑅)𝑞))⟩} ∈ V)
50		iunexg 6352	. . . . . . . . . . 11 ⊢ ((𝑉 ∈ V ∧ ∀𝑞 ∈ 𝑉 {⟨⟨(𝐹‘𝑝), (𝐹‘𝑞)⟩, (𝐹‘(𝑝(+g‘𝑅)𝑞))⟩} ∈ V) → ∪ 𝑞 ∈ 𝑉 {⟨⟨(𝐹‘𝑝), (𝐹‘𝑞)⟩, (𝐹‘(𝑝(+g‘𝑅)𝑞))⟩} ∈ V)
51	19, 49, 50	syl2anc 415	. . . . . . . . . 10 ⊢ (𝜑 → ∪ 𝑞 ∈ 𝑉 {⟨⟨(𝐹‘𝑝), (𝐹‘𝑞)⟩, (𝐹‘(𝑝(+g‘𝑅)𝑞))⟩} ∈ V)
52	51	ralrimivw 2624	. . . . . . . . 9 ⊢ (𝜑 → ∀𝑝 ∈ 𝑉 ∪ 𝑞 ∈ 𝑉 {⟨⟨(𝐹‘𝑝), (𝐹‘𝑞)⟩, (𝐹‘(𝑝(+g‘𝑅)𝑞))⟩} ∈ V)
53		iunexg 6352	. . . . . . . . 9 ⊢ ((𝑉 ∈ V ∧ ∀𝑝 ∈ 𝑉 ∪ 𝑞 ∈ 𝑉 {⟨⟨(𝐹‘𝑝), (𝐹‘𝑞)⟩, (𝐹‘(𝑝(+g‘𝑅)𝑞))⟩} ∈ V) → ∪ 𝑝 ∈ 𝑉 ∪ 𝑞 ∈ 𝑉 {⟨⟨(𝐹‘𝑝), (𝐹‘𝑞)⟩, (𝐹‘(𝑝(+g‘𝑅)𝑞))⟩} ∈ V)
54	19, 52, 53	syl2anc 415	. . . . . . . 8 ⊢ (𝜑 → ∪ 𝑝 ∈ 𝑉 ∪ 𝑞 ∈ 𝑉 {⟨⟨(𝐹‘𝑝), (𝐹‘𝑞)⟩, (𝐹‘(𝑝(+g‘𝑅)𝑞))⟩} ∈ V)
55		opexg 4370	. . . . . . . 8 ⊢ (((+g‘ndx) ∈ ℕ ∧ ∪ 𝑝 ∈ 𝑉 ∪ 𝑞 ∈ 𝑉 {⟨⟨(𝐹‘𝑝), (𝐹‘𝑞)⟩, (𝐹‘(𝑝(+g‘𝑅)𝑞))⟩} ∈ V) → ⟨(+g‘ndx), ∪ 𝑝 ∈ 𝑉 ∪ 𝑞 ∈ 𝑉 {⟨⟨(𝐹‘𝑝), (𝐹‘𝑞)⟩, (𝐹‘(𝑝(+g‘𝑅)𝑞))⟩}⟩ ∈ V)
56	24, 54, 55	sylancr 418	. . . . . . 7 ⊢ (𝜑 → ⟨(+g‘ndx), ∪ 𝑝 ∈ 𝑉 ∪ 𝑞 ∈ 𝑉 {⟨⟨(𝐹‘𝑝), (𝐹‘𝑞)⟩, (𝐹‘(𝑝(+g‘𝑅)𝑞))⟩}⟩ ∈ V)
57		mulrslid 13546	. . . . . . . . 9 ⊢ (.r = Slot (.r‘ndx) ∧ (.r‘ndx) ∈ ℕ)
58	57	simpri 113	. . . . . . . 8 ⊢ (.r‘ndx) ∈ ℕ
59	57	slotex 13438	. . . . . . . . . . . . . . . . 17 ⊢ (𝑅 ∈ 𝑍 → (.r‘𝑅) ∈ V)
60	10, 59	syl 14	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (.r‘𝑅) ∈ V)
61		ovexg 6122	. . . . . . . . . . . . . . . 16 ⊢ ((𝑝 ∈ V ∧ (.r‘𝑅) ∈ V ∧ 𝑞 ∈ V) → (𝑝(.r‘𝑅)𝑞) ∈ V)
62	36, 60, 40, 61	syl3anc 1278	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (𝑝(.r‘𝑅)𝑞) ∈ V)
63		fvexg 5717	. . . . . . . . . . . . . . 15 ⊢ ((𝐹 ∈ V ∧ (𝑝(.r‘𝑅)𝑞) ∈ V) → (𝐹‘(𝑝(.r‘𝑅)𝑞)) ∈ V)
64	27, 62, 63	syl2anc 415	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝐹‘(𝑝(.r‘𝑅)𝑞)) ∈ V)
65		opexg 4370	. . . . . . . . . . . . . 14 ⊢ ((⟨(𝐹‘𝑝), (𝐹‘𝑞)⟩ ∈ V ∧ (𝐹‘(𝑝(.r‘𝑅)𝑞)) ∈ V) → ⟨⟨(𝐹‘𝑝), (𝐹‘𝑞)⟩, (𝐹‘(𝑝(.r‘𝑅)𝑞))⟩ ∈ V)
66	35, 64, 65	syl2anc 415	. . . . . . . . . . . . 13 ⊢ (𝜑 → ⟨⟨(𝐹‘𝑝), (𝐹‘𝑞)⟩, (𝐹‘(𝑝(.r‘𝑅)𝑞))⟩ ∈ V)
67		snexg 4323	. . . . . . . . . . . . 13 ⊢ (⟨⟨(𝐹‘𝑝), (𝐹‘𝑞)⟩, (𝐹‘(𝑝(.r‘𝑅)𝑞))⟩ ∈ V → {⟨⟨(𝐹‘𝑝), (𝐹‘𝑞)⟩, (𝐹‘(𝑝(.r‘𝑅)𝑞))⟩} ∈ V)
68	66, 67	syl 14	. . . . . . . . . . . 12 ⊢ (𝜑 → {⟨⟨(𝐹‘𝑝), (𝐹‘𝑞)⟩, (𝐹‘(𝑝(.r‘𝑅)𝑞))⟩} ∈ V)
69	68	ralrimivw 2624	. . . . . . . . . . 11 ⊢ (𝜑 → ∀𝑞 ∈ 𝑉 {⟨⟨(𝐹‘𝑝), (𝐹‘𝑞)⟩, (𝐹‘(𝑝(.r‘𝑅)𝑞))⟩} ∈ V)
70		iunexg 6352	. . . . . . . . . . 11 ⊢ ((𝑉 ∈ V ∧ ∀𝑞 ∈ 𝑉 {⟨⟨(𝐹‘𝑝), (𝐹‘𝑞)⟩, (𝐹‘(𝑝(.r‘𝑅)𝑞))⟩} ∈ V) → ∪ 𝑞 ∈ 𝑉 {⟨⟨(𝐹‘𝑝), (𝐹‘𝑞)⟩, (𝐹‘(𝑝(.r‘𝑅)𝑞))⟩} ∈ V)
71	19, 69, 70	syl2anc 415	. . . . . . . . . 10 ⊢ (𝜑 → ∪ 𝑞 ∈ 𝑉 {⟨⟨(𝐹‘𝑝), (𝐹‘𝑞)⟩, (𝐹‘(𝑝(.r‘𝑅)𝑞))⟩} ∈ V)
72	71	ralrimivw 2624	. . . . . . . . 9 ⊢ (𝜑 → ∀𝑝 ∈ 𝑉 ∪ 𝑞 ∈ 𝑉 {⟨⟨(𝐹‘𝑝), (𝐹‘𝑞)⟩, (𝐹‘(𝑝(.r‘𝑅)𝑞))⟩} ∈ V)
73		iunexg 6352	. . . . . . . . 9 ⊢ ((𝑉 ∈ V ∧ ∀𝑝 ∈ 𝑉 ∪ 𝑞 ∈ 𝑉 {⟨⟨(𝐹‘𝑝), (𝐹‘𝑞)⟩, (𝐹‘(𝑝(.r‘𝑅)𝑞))⟩} ∈ V) → ∪ 𝑝 ∈ 𝑉 ∪ 𝑞 ∈ 𝑉 {⟨⟨(𝐹‘𝑝), (𝐹‘𝑞)⟩, (𝐹‘(𝑝(.r‘𝑅)𝑞))⟩} ∈ V)
74	19, 72, 73	syl2anc 415	. . . . . . . 8 ⊢ (𝜑 → ∪ 𝑝 ∈ 𝑉 ∪ 𝑞 ∈ 𝑉 {⟨⟨(𝐹‘𝑝), (𝐹‘𝑞)⟩, (𝐹‘(𝑝(.r‘𝑅)𝑞))⟩} ∈ V)
75		opexg 4370	. . . . . . . 8 ⊢ (((.r‘ndx) ∈ ℕ ∧ ∪ 𝑝 ∈ 𝑉 ∪ 𝑞 ∈ 𝑉 {⟨⟨(𝐹‘𝑝), (𝐹‘𝑞)⟩, (𝐹‘(𝑝(.r‘𝑅)𝑞))⟩} ∈ V) → ⟨(.r‘ndx), ∪ 𝑝 ∈ 𝑉 ∪ 𝑞 ∈ 𝑉 {⟨⟨(𝐹‘𝑝), (𝐹‘𝑞)⟩, (𝐹‘(𝑝(.r‘𝑅)𝑞))⟩}⟩ ∈ V)
76	58, 74, 75	sylancr 418	. . . . . . 7 ⊢ (𝜑 → ⟨(.r‘ndx), ∪ 𝑝 ∈ 𝑉 ∪ 𝑞 ∈ 𝑉 {⟨⟨(𝐹‘𝑝), (𝐹‘𝑞)⟩, (𝐹‘(𝑝(.r‘𝑅)𝑞))⟩}⟩ ∈ V)
77		tpexg 4592	. . . . . . 7 ⊢ ((⟨(Base‘ndx), 𝐵⟩ ∈ V ∧ ⟨(+g‘ndx), ∪ 𝑝 ∈ 𝑉 ∪ 𝑞 ∈ 𝑉 {⟨⟨(𝐹‘𝑝), (𝐹‘𝑞)⟩, (𝐹‘(𝑝(+g‘𝑅)𝑞))⟩}⟩ ∈ V ∧ ⟨(.r‘ndx), ∪ 𝑝 ∈ 𝑉 ∪ 𝑞 ∈ 𝑉 {⟨⟨(𝐹‘𝑝), (𝐹‘𝑞)⟩, (𝐹‘(𝑝(.r‘𝑅)𝑞))⟩}⟩ ∈ V) → {⟨(Base‘ndx), 𝐵⟩, ⟨(+g‘ndx), ∪ 𝑝 ∈ 𝑉 ∪ 𝑞 ∈ 𝑉 {⟨⟨(𝐹‘𝑝), (𝐹‘𝑞)⟩, (𝐹‘(𝑝(+g‘𝑅)𝑞))⟩}⟩, ⟨(.r‘ndx), ∪ 𝑝 ∈ 𝑉 ∪ 𝑞 ∈ 𝑉 {⟨⟨(𝐹‘𝑝), (𝐹‘𝑞)⟩, (𝐹‘(𝑝(.r‘𝑅)𝑞))⟩}⟩} ∈ V)
78	23, 56, 76, 77	syl3anc 1278	. . . . . 6 ⊢ (𝜑 → {⟨(Base‘ndx), 𝐵⟩, ⟨(+g‘ndx), ∪ 𝑝 ∈ 𝑉 ∪ 𝑞 ∈ 𝑉 {⟨⟨(𝐹‘𝑝), (𝐹‘𝑞)⟩, (𝐹‘(𝑝(+g‘𝑅)𝑞))⟩}⟩, ⟨(.r‘ndx), ∪ 𝑝 ∈ 𝑉 ∪ 𝑞 ∈ 𝑉 {⟨⟨(𝐹‘𝑝), (𝐹‘𝑞)⟩, (𝐹‘(𝑝(.r‘𝑅)𝑞))⟩}⟩} ∈ V)
79	11, 78	eqeltrd 2315	. . . . 5 ⊢ (𝜑 → 𝑈 ∈ V)
80		plusgid 13524	. . . . 5 ⊢ +g = Slot (+g‘ndx)
81	79, 80, 24	strndxid 13439	. . . 4 ⊢ (𝜑 → (𝑈‘(+g‘ndx)) = (+g‘𝑈))
82	24	a1i 9	. . . . 5 ⊢ (𝜑 → (+g‘ndx) ∈ ℕ)
83		basendxnplusgndx 13539	. . . . . 6 ⊢ (Base‘ndx) ≠ (+g‘ndx)
84	83	a1i 9	. . . . 5 ⊢ (𝜑 → (Base‘ndx) ≠ (+g‘ndx))
85		plusgndxnmulrndx 13547	. . . . . 6 ⊢ (+g‘ndx) ≠ (.r‘ndx)
86	85	a1i 9	. . . . 5 ⊢ (𝜑 → (+g‘ndx) ≠ (.r‘ndx))
87		fvtp2g 5927	. . . . 5 ⊢ ((((+g‘ndx) ∈ ℕ ∧ ∪ 𝑝 ∈ 𝑉 ∪ 𝑞 ∈ 𝑉 {⟨⟨(𝐹‘𝑝), (𝐹‘𝑞)⟩, (𝐹‘(𝑝(+g‘𝑅)𝑞))⟩} ∈ V) ∧ ((Base‘ndx) ≠ (+g‘ndx) ∧ (+g‘ndx) ≠ (.r‘ndx))) → ({⟨(Base‘ndx), 𝐵⟩, ⟨(+g‘ndx), ∪ 𝑝 ∈ 𝑉 ∪ 𝑞 ∈ 𝑉 {⟨⟨(𝐹‘𝑝), (𝐹‘𝑞)⟩, (𝐹‘(𝑝(+g‘𝑅)𝑞))⟩}⟩, ⟨(.r‘ndx), ∪ 𝑝 ∈ 𝑉 ∪ 𝑞 ∈ 𝑉 {⟨⟨(𝐹‘𝑝), (𝐹‘𝑞)⟩, (𝐹‘(𝑝(.r‘𝑅)𝑞))⟩}⟩}‘(+g‘ndx)) = ∪ 𝑝 ∈ 𝑉 ∪ 𝑞 ∈ 𝑉 {⟨⟨(𝐹‘𝑝), (𝐹‘𝑞)⟩, (𝐹‘(𝑝(+g‘𝑅)𝑞))⟩})
88	82, 54, 84, 86, 87	syl22anc 1279	. . . 4 ⊢ (𝜑 → ({⟨(Base‘ndx), 𝐵⟩, ⟨(+g‘ndx), ∪ 𝑝 ∈ 𝑉 ∪ 𝑞 ∈ 𝑉 {⟨⟨(𝐹‘𝑝), (𝐹‘𝑞)⟩, (𝐹‘(𝑝(+g‘𝑅)𝑞))⟩}⟩, ⟨(.r‘ndx), ∪ 𝑝 ∈ 𝑉 ∪ 𝑞 ∈ 𝑉 {⟨⟨(𝐹‘𝑝), (𝐹‘𝑞)⟩, (𝐹‘(𝑝(.r‘𝑅)𝑞))⟩}⟩}‘(+g‘ndx)) = ∪ 𝑝 ∈ 𝑉 ∪ 𝑞 ∈ 𝑉 {⟨⟨(𝐹‘𝑝), (𝐹‘𝑞)⟩, (𝐹‘(𝑝(+g‘𝑅)𝑞))⟩})
89	12, 81, 88	3eqtr3rd 2280	. . 3 ⊢ (𝜑 → ∪ 𝑝 ∈ 𝑉 ∪ 𝑞 ∈ 𝑉 {⟨⟨(𝐹‘𝑝), (𝐹‘𝑞)⟩, (𝐹‘(𝑝(+g‘𝑅)𝑞))⟩} = (+g‘𝑈))
90	1, 89	eqtr4id 2290	. 2 ⊢ (𝜑 → + = ∪ 𝑝 ∈ 𝑉 ∪ 𝑞 ∈ 𝑉 {⟨⟨(𝐹‘𝑝), (𝐹‘𝑞)⟩, (𝐹‘(𝑝(+g‘𝑅)𝑞))⟩})
91		imasplusg.p	. . . . . . . . . 10 ⊢ + = (+g‘𝑅)
92	91	oveqi 6101	. . . . . . . . 9 ⊢ (𝑝 + 𝑞) = (𝑝(+g‘𝑅)𝑞)
93	92	fveq2i 5701	. . . . . . . 8 ⊢ (𝐹‘(𝑝 + 𝑞)) = (𝐹‘(𝑝(+g‘𝑅)𝑞))
94	93	opeq2i 3908	. . . . . . 7 ⊢ ⟨⟨(𝐹‘𝑝), (𝐹‘𝑞)⟩, (𝐹‘(𝑝 + 𝑞))⟩ = ⟨⟨(𝐹‘𝑝), (𝐹‘𝑞)⟩, (𝐹‘(𝑝(+g‘𝑅)𝑞))⟩
95	94	sneqi 3721	. . . . . 6 ⊢ {⟨⟨(𝐹‘𝑝), (𝐹‘𝑞)⟩, (𝐹‘(𝑝 + 𝑞))⟩} = {⟨⟨(𝐹‘𝑝), (𝐹‘𝑞)⟩, (𝐹‘(𝑝(+g‘𝑅)𝑞))⟩}
96	95	a1i 9	. . . . 5 ⊢ (𝑞 ∈ 𝑉 → {⟨⟨(𝐹‘𝑝), (𝐹‘𝑞)⟩, (𝐹‘(𝑝 + 𝑞))⟩} = {⟨⟨(𝐹‘𝑝), (𝐹‘𝑞)⟩, (𝐹‘(𝑝(+g‘𝑅)𝑞))⟩})
97	96	iuneq2i 4030	. . . 4 ⊢ ∪ 𝑞 ∈ 𝑉 {⟨⟨(𝐹‘𝑝), (𝐹‘𝑞)⟩, (𝐹‘(𝑝 + 𝑞))⟩} = ∪ 𝑞 ∈ 𝑉 {⟨⟨(𝐹‘𝑝), (𝐹‘𝑞)⟩, (𝐹‘(𝑝(+g‘𝑅)𝑞))⟩}
98	97	a1i 9	. . 3 ⊢ (𝑝 ∈ 𝑉 → ∪ 𝑞 ∈ 𝑉 {⟨⟨(𝐹‘𝑝), (𝐹‘𝑞)⟩, (𝐹‘(𝑝 + 𝑞))⟩} = ∪ 𝑞 ∈ 𝑉 {⟨⟨(𝐹‘𝑝), (𝐹‘𝑞)⟩, (𝐹‘(𝑝(+g‘𝑅)𝑞))⟩})
99	98	iuneq2i 4030	. 2 ⊢ ∪ 𝑝 ∈ 𝑉 ∪ 𝑞 ∈ 𝑉 {⟨⟨(𝐹‘𝑝), (𝐹‘𝑞)⟩, (𝐹‘(𝑝 + 𝑞))⟩} = ∪ 𝑝 ∈ 𝑉 ∪ 𝑞 ∈ 𝑉 {⟨⟨(𝐹‘𝑝), (𝐹‘𝑞)⟩, (𝐹‘(𝑝(+g‘𝑅)𝑞))⟩}
100	90, 99	eqtr4di 2289	1 ⊢ (𝜑 → + = ∪ 𝑝 ∈ 𝑉 ∪ 𝑞 ∈ 𝑉 {⟨⟨(𝐹‘𝑝), (𝐹‘𝑞)⟩, (𝐹‘(𝑝 + 𝑞))⟩})

This proof depends on syntax axioms:   → wi 4   = wceq 1402   ∈ wcel 2209   ≠ wne 2420  ∀wral 2528  Vcvv 2821  {csn 3709  {ctp 3711  ⟨cop 3712  ∪ ciun 4012   Fn wfn 5375  ⟶wf 5376  –onto→wfo 5378  ‘cfv 5380  (class class class)co 6088  ℕcn 9314  ndxcnx 13408  Slot cslot 13410  Basecbs 13411  +_gcplusg 13491  ._rcmulr 13492   ·_𝑠 cvsca 13495   “_s cimas 13682

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-in1 623  ax-in2 624  ax-io 721  ax-5 1500  ax-7 1501  ax-gen 1502  ax-ie1 1546  ax-ie2 1547  ax-8 1557  ax-10 1558  ax-11 1559  ax-i12 1560  ax-bndl 1562  ax-4 1563  ax-17 1579  ax-i9 1583  ax-ial 1587  ax-i5r 1588  ax-14 2212  ax-ext 2220  ax-coll 4248  ax-sep 4251  ax-pow 4313  ax-pr 4348  ax-un 4580  ax-setind 4686  ax-cnex 8277  ax-resscn 8278  ax-1cn 8279  ax-1re 8280  ax-icn 8281  ax-addcl 8282  ax-addrcl 8283  ax-mulcl 8284  ax-addcom 8286  ax-addass 8288  ax-i2m1 8291  ax-0lt1 8292  ax-0id 8294  ax-rnegex 8295  ax-pre-ltirr 8298  ax-pre-ltadd 8302

This proof depends on definitions:  df-bi 117  df-3or 1010  df-3an 1011  df-tru 1405  df-fal 1408  df-nf 1514  df-sb 1816  df-eu 2089  df-mo 2090  df-clab 2225  df-cleq 2231  df-clel 2234  df-nfc 2381  df-ne 2421  df-nel 2516  df-ral 2533  df-rex 2534  df-reu 2535  df-rab 2537  df-v 2823  df-sbc 3052  df-csb 3148  df-dif 3222  df-un 3224  df-in 3226  df-ss 3233  df-nul 3521  df-pw 3690  df-sn 3715  df-pr 3716  df-tp 3717  df-op 3718  df-uni 3936  df-int 3971  df-iun 4014  df-br 4132  df-opab 4194  df-mpt 4195  df-id 4440  df-xp 4782  df-rel 4783  df-cnv 4784  df-co 4785  df-dm 4786  df-rn 4787  df-res 4788  df-ima 4789  df-iota 5340  df-fun 5382  df-fn 5383  df-f 5384  df-f1 5385  df-fo 5386  df-f1o 5387  df-fv 5388  df-ov 6091  df-oprab 6092  df-mpo 6093  df-pnf 8369  df-mnf 8370  df-ltxr 8372  df-inn 9315  df-2 9373  df-3 9374  df-ndx 13414  df-slot 13415  df-base 13417  df-plusg 13504  df-mulr 13505  df-iimas 13684

This theorem is used by:  imasaddfn  13698  imasaddval  13699  imasaddf  13700  qusaddval  13716  qusaddf  13717