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

Theorem psgnunilem3 19285
Description: Lemma for psgnuni 19288. Any nonempty representation of the identity can be incrementally transformed into a representation two shorter. (Contributed by Stefan O'Rear, 25-Aug-2015.)
Hypotheses
Ref Expression
psgnunilem3.g 𝐺 = (SymGrpβ€˜π·)
psgnunilem3.t 𝑇 = ran (pmTrspβ€˜π·)
psgnunilem3.d (πœ‘ β†’ 𝐷 ∈ 𝑉)
psgnunilem3.w1 (πœ‘ β†’ π‘Š ∈ Word 𝑇)
psgnunilem3.l (πœ‘ β†’ (β™―β€˜π‘Š) = 𝐿)
psgnunilem3.w2 (πœ‘ β†’ (β™―β€˜π‘Š) ∈ β„•)
psgnunilem3.w3 (πœ‘ β†’ (𝐺 Ξ£g π‘Š) = ( I β†Ύ 𝐷))
psgnunilem3.in (πœ‘ β†’ Β¬ βˆƒπ‘₯ ∈ Word 𝑇((β™―β€˜π‘₯) = (𝐿 βˆ’ 2) ∧ (𝐺 Ξ£g π‘₯) = ( I β†Ύ 𝐷)))
Assertion
Ref Expression
psgnunilem3 Β¬ πœ‘
Distinct variable groups:   π‘₯,𝐷   π‘₯,𝐺   π‘₯,𝐿   π‘₯,𝑇   π‘₯,π‘Š   πœ‘,π‘₯
Allowed substitution hint:   𝑉(π‘₯)

Proof of Theorem psgnunilem3
Dummy variables π‘Ž 𝑏 𝑐 𝑑 𝑒 𝑀 𝑦 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 psgnunilem3.l . . . 4 (πœ‘ β†’ (β™―β€˜π‘Š) = 𝐿)
2 psgnunilem3.w2 . . . 4 (πœ‘ β†’ (β™―β€˜π‘Š) ∈ β„•)
31, 2eqeltrrd 2839 . . 3 (πœ‘ β†’ 𝐿 ∈ β„•)
43nnnn0d 12480 . 2 (πœ‘ β†’ 𝐿 ∈ β„•0)
5 psgnunilem3.w1 . . . . . . 7 (πœ‘ β†’ π‘Š ∈ Word 𝑇)
6 wrdf 14414 . . . . . . 7 (π‘Š ∈ Word 𝑇 β†’ π‘Š:(0..^(β™―β€˜π‘Š))βŸΆπ‘‡)
75, 6syl 17 . . . . . 6 (πœ‘ β†’ π‘Š:(0..^(β™―β€˜π‘Š))βŸΆπ‘‡)
8 0nn0 12435 . . . . . . . . 9 0 ∈ β„•0
98a1i 11 . . . . . . . 8 (πœ‘ β†’ 0 ∈ β„•0)
103nngt0d 12209 . . . . . . . 8 (πœ‘ β†’ 0 < 𝐿)
11 elfzo0 13620 . . . . . . . 8 (0 ∈ (0..^𝐿) ↔ (0 ∈ β„•0 ∧ 𝐿 ∈ β„• ∧ 0 < 𝐿))
129, 3, 10, 11syl3anbrc 1344 . . . . . . 7 (πœ‘ β†’ 0 ∈ (0..^𝐿))
131oveq2d 7378 . . . . . . 7 (πœ‘ β†’ (0..^(β™―β€˜π‘Š)) = (0..^𝐿))
1412, 13eleqtrrd 2841 . . . . . 6 (πœ‘ β†’ 0 ∈ (0..^(β™―β€˜π‘Š)))
157, 14ffvelcdmd 7041 . . . . 5 (πœ‘ β†’ (π‘Šβ€˜0) ∈ 𝑇)
16 eqid 2737 . . . . . 6 (pmTrspβ€˜π·) = (pmTrspβ€˜π·)
17 psgnunilem3.t . . . . . 6 𝑇 = ran (pmTrspβ€˜π·)
1816, 17pmtrfmvdn0 19251 . . . . 5 ((π‘Šβ€˜0) ∈ 𝑇 β†’ dom ((π‘Šβ€˜0) βˆ– I ) β‰  βˆ…)
1915, 18syl 17 . . . 4 (πœ‘ β†’ dom ((π‘Šβ€˜0) βˆ– I ) β‰  βˆ…)
20 n0 4311 . . . 4 (dom ((π‘Šβ€˜0) βˆ– I ) β‰  βˆ… ↔ βˆƒπ‘’ 𝑒 ∈ dom ((π‘Šβ€˜0) βˆ– I ))
2119, 20sylib 217 . . 3 (πœ‘ β†’ βˆƒπ‘’ 𝑒 ∈ dom ((π‘Šβ€˜0) βˆ– I ))
22 fzonel 13593 . . . . . . . 8 Β¬ 𝐿 ∈ (0..^𝐿)
23 simpr1 1195 . . . . . . . 8 ((((𝐺 Ξ£g 𝑀) = ( I β†Ύ 𝐷) ∧ (β™―β€˜π‘€) = 𝐿) ∧ (𝐿 ∈ (0..^𝐿) ∧ 𝑒 ∈ dom ((π‘€β€˜πΏ) βˆ– I ) ∧ βˆ€π‘ ∈ (0..^𝐿) Β¬ 𝑒 ∈ dom ((π‘€β€˜π‘) βˆ– I ))) β†’ 𝐿 ∈ (0..^𝐿))
2422, 23mto 196 . . . . . . 7 Β¬ (((𝐺 Ξ£g 𝑀) = ( I β†Ύ 𝐷) ∧ (β™―β€˜π‘€) = 𝐿) ∧ (𝐿 ∈ (0..^𝐿) ∧ 𝑒 ∈ dom ((π‘€β€˜πΏ) βˆ– I ) ∧ βˆ€π‘ ∈ (0..^𝐿) Β¬ 𝑒 ∈ dom ((π‘€β€˜π‘) βˆ– I )))
2524a1i 11 . . . . . 6 (𝑀 ∈ Word 𝑇 β†’ Β¬ (((𝐺 Ξ£g 𝑀) = ( I β†Ύ 𝐷) ∧ (β™―β€˜π‘€) = 𝐿) ∧ (𝐿 ∈ (0..^𝐿) ∧ 𝑒 ∈ dom ((π‘€β€˜πΏ) βˆ– I ) ∧ βˆ€π‘ ∈ (0..^𝐿) Β¬ 𝑒 ∈ dom ((π‘€β€˜π‘) βˆ– I ))))
2625nrex 3078 . . . . 5 Β¬ βˆƒπ‘€ ∈ Word 𝑇(((𝐺 Ξ£g 𝑀) = ( I β†Ύ 𝐷) ∧ (β™―β€˜π‘€) = 𝐿) ∧ (𝐿 ∈ (0..^𝐿) ∧ 𝑒 ∈ dom ((π‘€β€˜πΏ) βˆ– I ) ∧ βˆ€π‘ ∈ (0..^𝐿) Β¬ 𝑒 ∈ dom ((π‘€β€˜π‘) βˆ– I )))
27 eleq1 2826 . . . . . . . . . 10 (π‘Ž = 0 β†’ (π‘Ž ∈ (0..^𝐿) ↔ 0 ∈ (0..^𝐿)))
28 fveq2 6847 . . . . . . . . . . . . 13 (π‘Ž = 0 β†’ (π‘€β€˜π‘Ž) = (π‘€β€˜0))
2928difeq1d 4086 . . . . . . . . . . . 12 (π‘Ž = 0 β†’ ((π‘€β€˜π‘Ž) βˆ– I ) = ((π‘€β€˜0) βˆ– I ))
3029dmeqd 5866 . . . . . . . . . . 11 (π‘Ž = 0 β†’ dom ((π‘€β€˜π‘Ž) βˆ– I ) = dom ((π‘€β€˜0) βˆ– I ))
3130eleq2d 2824 . . . . . . . . . 10 (π‘Ž = 0 β†’ (𝑒 ∈ dom ((π‘€β€˜π‘Ž) βˆ– I ) ↔ 𝑒 ∈ dom ((π‘€β€˜0) βˆ– I )))
32 oveq2 7370 . . . . . . . . . . 11 (π‘Ž = 0 β†’ (0..^π‘Ž) = (0..^0))
3332raleqdv 3316 . . . . . . . . . 10 (π‘Ž = 0 β†’ (βˆ€π‘ ∈ (0..^π‘Ž) Β¬ 𝑒 ∈ dom ((π‘€β€˜π‘) βˆ– I ) ↔ βˆ€π‘ ∈ (0..^0) Β¬ 𝑒 ∈ dom ((π‘€β€˜π‘) βˆ– I )))
3427, 31, 333anbi123d 1437 . . . . . . . . 9 (π‘Ž = 0 β†’ ((π‘Ž ∈ (0..^𝐿) ∧ 𝑒 ∈ dom ((π‘€β€˜π‘Ž) βˆ– I ) ∧ βˆ€π‘ ∈ (0..^π‘Ž) Β¬ 𝑒 ∈ dom ((π‘€β€˜π‘) βˆ– I )) ↔ (0 ∈ (0..^𝐿) ∧ 𝑒 ∈ dom ((π‘€β€˜0) βˆ– I ) ∧ βˆ€π‘ ∈ (0..^0) Β¬ 𝑒 ∈ dom ((π‘€β€˜π‘) βˆ– I ))))
3534anbi2d 630 . . . . . . . 8 (π‘Ž = 0 β†’ ((((𝐺 Ξ£g 𝑀) = ( I β†Ύ 𝐷) ∧ (β™―β€˜π‘€) = 𝐿) ∧ (π‘Ž ∈ (0..^𝐿) ∧ 𝑒 ∈ dom ((π‘€β€˜π‘Ž) βˆ– I ) ∧ βˆ€π‘ ∈ (0..^π‘Ž) Β¬ 𝑒 ∈ dom ((π‘€β€˜π‘) βˆ– I ))) ↔ (((𝐺 Ξ£g 𝑀) = ( I β†Ύ 𝐷) ∧ (β™―β€˜π‘€) = 𝐿) ∧ (0 ∈ (0..^𝐿) ∧ 𝑒 ∈ dom ((π‘€β€˜0) βˆ– I ) ∧ βˆ€π‘ ∈ (0..^0) Β¬ 𝑒 ∈ dom ((π‘€β€˜π‘) βˆ– I )))))
3635rexbidv 3176 . . . . . . 7 (π‘Ž = 0 β†’ (βˆƒπ‘€ ∈ Word 𝑇(((𝐺 Ξ£g 𝑀) = ( I β†Ύ 𝐷) ∧ (β™―β€˜π‘€) = 𝐿) ∧ (π‘Ž ∈ (0..^𝐿) ∧ 𝑒 ∈ dom ((π‘€β€˜π‘Ž) βˆ– I ) ∧ βˆ€π‘ ∈ (0..^π‘Ž) Β¬ 𝑒 ∈ dom ((π‘€β€˜π‘) βˆ– I ))) ↔ βˆƒπ‘€ ∈ Word 𝑇(((𝐺 Ξ£g 𝑀) = ( I β†Ύ 𝐷) ∧ (β™―β€˜π‘€) = 𝐿) ∧ (0 ∈ (0..^𝐿) ∧ 𝑒 ∈ dom ((π‘€β€˜0) βˆ– I ) ∧ βˆ€π‘ ∈ (0..^0) Β¬ 𝑒 ∈ dom ((π‘€β€˜π‘) βˆ– I )))))
3736imbi2d 341 . . . . . 6 (π‘Ž = 0 β†’ (((πœ‘ ∧ 𝑒 ∈ dom ((π‘Šβ€˜0) βˆ– I )) β†’ βˆƒπ‘€ ∈ Word 𝑇(((𝐺 Ξ£g 𝑀) = ( I β†Ύ 𝐷) ∧ (β™―β€˜π‘€) = 𝐿) ∧ (π‘Ž ∈ (0..^𝐿) ∧ 𝑒 ∈ dom ((π‘€β€˜π‘Ž) βˆ– I ) ∧ βˆ€π‘ ∈ (0..^π‘Ž) Β¬ 𝑒 ∈ dom ((π‘€β€˜π‘) βˆ– I )))) ↔ ((πœ‘ ∧ 𝑒 ∈ dom ((π‘Šβ€˜0) βˆ– I )) β†’ βˆƒπ‘€ ∈ Word 𝑇(((𝐺 Ξ£g 𝑀) = ( I β†Ύ 𝐷) ∧ (β™―β€˜π‘€) = 𝐿) ∧ (0 ∈ (0..^𝐿) ∧ 𝑒 ∈ dom ((π‘€β€˜0) βˆ– I ) ∧ βˆ€π‘ ∈ (0..^0) Β¬ 𝑒 ∈ dom ((π‘€β€˜π‘) βˆ– I ))))))
38 eleq1 2826 . . . . . . . . . . 11 (π‘Ž = 𝑏 β†’ (π‘Ž ∈ (0..^𝐿) ↔ 𝑏 ∈ (0..^𝐿)))
39 fveq2 6847 . . . . . . . . . . . . . 14 (π‘Ž = 𝑏 β†’ (π‘€β€˜π‘Ž) = (π‘€β€˜π‘))
4039difeq1d 4086 . . . . . . . . . . . . 13 (π‘Ž = 𝑏 β†’ ((π‘€β€˜π‘Ž) βˆ– I ) = ((π‘€β€˜π‘) βˆ– I ))
4140dmeqd 5866 . . . . . . . . . . . 12 (π‘Ž = 𝑏 β†’ dom ((π‘€β€˜π‘Ž) βˆ– I ) = dom ((π‘€β€˜π‘) βˆ– I ))
4241eleq2d 2824 . . . . . . . . . . 11 (π‘Ž = 𝑏 β†’ (𝑒 ∈ dom ((π‘€β€˜π‘Ž) βˆ– I ) ↔ 𝑒 ∈ dom ((π‘€β€˜π‘) βˆ– I )))
43 oveq2 7370 . . . . . . . . . . . 12 (π‘Ž = 𝑏 β†’ (0..^π‘Ž) = (0..^𝑏))
4443raleqdv 3316 . . . . . . . . . . 11 (π‘Ž = 𝑏 β†’ (βˆ€π‘ ∈ (0..^π‘Ž) Β¬ 𝑒 ∈ dom ((π‘€β€˜π‘) βˆ– I ) ↔ βˆ€π‘ ∈ (0..^𝑏) Β¬ 𝑒 ∈ dom ((π‘€β€˜π‘) βˆ– I )))
4538, 42, 443anbi123d 1437 . . . . . . . . . 10 (π‘Ž = 𝑏 β†’ ((π‘Ž ∈ (0..^𝐿) ∧ 𝑒 ∈ dom ((π‘€β€˜π‘Ž) βˆ– I ) ∧ βˆ€π‘ ∈ (0..^π‘Ž) Β¬ 𝑒 ∈ dom ((π‘€β€˜π‘) βˆ– I )) ↔ (𝑏 ∈ (0..^𝐿) ∧ 𝑒 ∈ dom ((π‘€β€˜π‘) βˆ– I ) ∧ βˆ€π‘ ∈ (0..^𝑏) Β¬ 𝑒 ∈ dom ((π‘€β€˜π‘) βˆ– I ))))
4645anbi2d 630 . . . . . . . . 9 (π‘Ž = 𝑏 β†’ ((((𝐺 Ξ£g 𝑀) = ( I β†Ύ 𝐷) ∧ (β™―β€˜π‘€) = 𝐿) ∧ (π‘Ž ∈ (0..^𝐿) ∧ 𝑒 ∈ dom ((π‘€β€˜π‘Ž) βˆ– I ) ∧ βˆ€π‘ ∈ (0..^π‘Ž) Β¬ 𝑒 ∈ dom ((π‘€β€˜π‘) βˆ– I ))) ↔ (((𝐺 Ξ£g 𝑀) = ( I β†Ύ 𝐷) ∧ (β™―β€˜π‘€) = 𝐿) ∧ (𝑏 ∈ (0..^𝐿) ∧ 𝑒 ∈ dom ((π‘€β€˜π‘) βˆ– I ) ∧ βˆ€π‘ ∈ (0..^𝑏) Β¬ 𝑒 ∈ dom ((π‘€β€˜π‘) βˆ– I )))))
4746rexbidv 3176 . . . . . . . 8 (π‘Ž = 𝑏 β†’ (βˆƒπ‘€ ∈ Word 𝑇(((𝐺 Ξ£g 𝑀) = ( I β†Ύ 𝐷) ∧ (β™―β€˜π‘€) = 𝐿) ∧ (π‘Ž ∈ (0..^𝐿) ∧ 𝑒 ∈ dom ((π‘€β€˜π‘Ž) βˆ– I ) ∧ βˆ€π‘ ∈ (0..^π‘Ž) Β¬ 𝑒 ∈ dom ((π‘€β€˜π‘) βˆ– I ))) ↔ βˆƒπ‘€ ∈ Word 𝑇(((𝐺 Ξ£g 𝑀) = ( I β†Ύ 𝐷) ∧ (β™―β€˜π‘€) = 𝐿) ∧ (𝑏 ∈ (0..^𝐿) ∧ 𝑒 ∈ dom ((π‘€β€˜π‘) βˆ– I ) ∧ βˆ€π‘ ∈ (0..^𝑏) Β¬ 𝑒 ∈ dom ((π‘€β€˜π‘) βˆ– I )))))
48 oveq2 7370 . . . . . . . . . . . 12 (𝑀 = π‘₯ β†’ (𝐺 Ξ£g 𝑀) = (𝐺 Ξ£g π‘₯))
4948eqeq1d 2739 . . . . . . . . . . 11 (𝑀 = π‘₯ β†’ ((𝐺 Ξ£g 𝑀) = ( I β†Ύ 𝐷) ↔ (𝐺 Ξ£g π‘₯) = ( I β†Ύ 𝐷)))
50 fveqeq2 6856 . . . . . . . . . . 11 (𝑀 = π‘₯ β†’ ((β™―β€˜π‘€) = 𝐿 ↔ (β™―β€˜π‘₯) = 𝐿))
5149, 50anbi12d 632 . . . . . . . . . 10 (𝑀 = π‘₯ β†’ (((𝐺 Ξ£g 𝑀) = ( I β†Ύ 𝐷) ∧ (β™―β€˜π‘€) = 𝐿) ↔ ((𝐺 Ξ£g π‘₯) = ( I β†Ύ 𝐷) ∧ (β™―β€˜π‘₯) = 𝐿)))
52 fveq1 6846 . . . . . . . . . . . . . 14 (𝑀 = π‘₯ β†’ (π‘€β€˜π‘) = (π‘₯β€˜π‘))
5352difeq1d 4086 . . . . . . . . . . . . 13 (𝑀 = π‘₯ β†’ ((π‘€β€˜π‘) βˆ– I ) = ((π‘₯β€˜π‘) βˆ– I ))
5453dmeqd 5866 . . . . . . . . . . . 12 (𝑀 = π‘₯ β†’ dom ((π‘€β€˜π‘) βˆ– I ) = dom ((π‘₯β€˜π‘) βˆ– I ))
5554eleq2d 2824 . . . . . . . . . . 11 (𝑀 = π‘₯ β†’ (𝑒 ∈ dom ((π‘€β€˜π‘) βˆ– I ) ↔ 𝑒 ∈ dom ((π‘₯β€˜π‘) βˆ– I )))
56 fveq1 6846 . . . . . . . . . . . . . . . . 17 (𝑀 = π‘₯ β†’ (π‘€β€˜π‘) = (π‘₯β€˜π‘))
5756difeq1d 4086 . . . . . . . . . . . . . . . 16 (𝑀 = π‘₯ β†’ ((π‘€β€˜π‘) βˆ– I ) = ((π‘₯β€˜π‘) βˆ– I ))
5857dmeqd 5866 . . . . . . . . . . . . . . 15 (𝑀 = π‘₯ β†’ dom ((π‘€β€˜π‘) βˆ– I ) = dom ((π‘₯β€˜π‘) βˆ– I ))
5958eleq2d 2824 . . . . . . . . . . . . . 14 (𝑀 = π‘₯ β†’ (𝑒 ∈ dom ((π‘€β€˜π‘) βˆ– I ) ↔ 𝑒 ∈ dom ((π‘₯β€˜π‘) βˆ– I )))
6059notbid 318 . . . . . . . . . . . . 13 (𝑀 = π‘₯ β†’ (Β¬ 𝑒 ∈ dom ((π‘€β€˜π‘) βˆ– I ) ↔ Β¬ 𝑒 ∈ dom ((π‘₯β€˜π‘) βˆ– I )))
6160ralbidv 3175 . . . . . . . . . . . 12 (𝑀 = π‘₯ β†’ (βˆ€π‘ ∈ (0..^𝑏) Β¬ 𝑒 ∈ dom ((π‘€β€˜π‘) βˆ– I ) ↔ βˆ€π‘ ∈ (0..^𝑏) Β¬ 𝑒 ∈ dom ((π‘₯β€˜π‘) βˆ– I )))
62 fveq2 6847 . . . . . . . . . . . . . . . . 17 (𝑐 = 𝑑 β†’ (π‘₯β€˜π‘) = (π‘₯β€˜π‘‘))
6362difeq1d 4086 . . . . . . . . . . . . . . . 16 (𝑐 = 𝑑 β†’ ((π‘₯β€˜π‘) βˆ– I ) = ((π‘₯β€˜π‘‘) βˆ– I ))
6463dmeqd 5866 . . . . . . . . . . . . . . 15 (𝑐 = 𝑑 β†’ dom ((π‘₯β€˜π‘) βˆ– I ) = dom ((π‘₯β€˜π‘‘) βˆ– I ))
6564eleq2d 2824 . . . . . . . . . . . . . 14 (𝑐 = 𝑑 β†’ (𝑒 ∈ dom ((π‘₯β€˜π‘) βˆ– I ) ↔ 𝑒 ∈ dom ((π‘₯β€˜π‘‘) βˆ– I )))
6665notbid 318 . . . . . . . . . . . . 13 (𝑐 = 𝑑 β†’ (Β¬ 𝑒 ∈ dom ((π‘₯β€˜π‘) βˆ– I ) ↔ Β¬ 𝑒 ∈ dom ((π‘₯β€˜π‘‘) βˆ– I )))
6766cbvralvw 3228 . . . . . . . . . . . 12 (βˆ€π‘ ∈ (0..^𝑏) Β¬ 𝑒 ∈ dom ((π‘₯β€˜π‘) βˆ– I ) ↔ βˆ€π‘‘ ∈ (0..^𝑏) Β¬ 𝑒 ∈ dom ((π‘₯β€˜π‘‘) βˆ– I ))
6861, 67bitrdi 287 . . . . . . . . . . 11 (𝑀 = π‘₯ β†’ (βˆ€π‘ ∈ (0..^𝑏) Β¬ 𝑒 ∈ dom ((π‘€β€˜π‘) βˆ– I ) ↔ βˆ€π‘‘ ∈ (0..^𝑏) Β¬ 𝑒 ∈ dom ((π‘₯β€˜π‘‘) βˆ– I )))
6955, 683anbi23d 1440 . . . . . . . . . 10 (𝑀 = π‘₯ β†’ ((𝑏 ∈ (0..^𝐿) ∧ 𝑒 ∈ dom ((π‘€β€˜π‘) βˆ– I ) ∧ βˆ€π‘ ∈ (0..^𝑏) Β¬ 𝑒 ∈ dom ((π‘€β€˜π‘) βˆ– I )) ↔ (𝑏 ∈ (0..^𝐿) ∧ 𝑒 ∈ dom ((π‘₯β€˜π‘) βˆ– I ) ∧ βˆ€π‘‘ ∈ (0..^𝑏) Β¬ 𝑒 ∈ dom ((π‘₯β€˜π‘‘) βˆ– I ))))
7051, 69anbi12d 632 . . . . . . . . 9 (𝑀 = π‘₯ β†’ ((((𝐺 Ξ£g 𝑀) = ( I β†Ύ 𝐷) ∧ (β™―β€˜π‘€) = 𝐿) ∧ (𝑏 ∈ (0..^𝐿) ∧ 𝑒 ∈ dom ((π‘€β€˜π‘) βˆ– I ) ∧ βˆ€π‘ ∈ (0..^𝑏) Β¬ 𝑒 ∈ dom ((π‘€β€˜π‘) βˆ– I ))) ↔ (((𝐺 Ξ£g π‘₯) = ( I β†Ύ 𝐷) ∧ (β™―β€˜π‘₯) = 𝐿) ∧ (𝑏 ∈ (0..^𝐿) ∧ 𝑒 ∈ dom ((π‘₯β€˜π‘) βˆ– I ) ∧ βˆ€π‘‘ ∈ (0..^𝑏) Β¬ 𝑒 ∈ dom ((π‘₯β€˜π‘‘) βˆ– I )))))
7170cbvrexvw 3229 . . . . . . . 8 (βˆƒπ‘€ ∈ Word 𝑇(((𝐺 Ξ£g 𝑀) = ( I β†Ύ 𝐷) ∧ (β™―β€˜π‘€) = 𝐿) ∧ (𝑏 ∈ (0..^𝐿) ∧ 𝑒 ∈ dom ((π‘€β€˜π‘) βˆ– I ) ∧ βˆ€π‘ ∈ (0..^𝑏) Β¬ 𝑒 ∈ dom ((π‘€β€˜π‘) βˆ– I ))) ↔ βˆƒπ‘₯ ∈ Word 𝑇(((𝐺 Ξ£g π‘₯) = ( I β†Ύ 𝐷) ∧ (β™―β€˜π‘₯) = 𝐿) ∧ (𝑏 ∈ (0..^𝐿) ∧ 𝑒 ∈ dom ((π‘₯β€˜π‘) βˆ– I ) ∧ βˆ€π‘‘ ∈ (0..^𝑏) Β¬ 𝑒 ∈ dom ((π‘₯β€˜π‘‘) βˆ– I ))))
7247, 71bitrdi 287 . . . . . . 7 (π‘Ž = 𝑏 β†’ (βˆƒπ‘€ ∈ Word 𝑇(((𝐺 Ξ£g 𝑀) = ( I β†Ύ 𝐷) ∧ (β™―β€˜π‘€) = 𝐿) ∧ (π‘Ž ∈ (0..^𝐿) ∧ 𝑒 ∈ dom ((π‘€β€˜π‘Ž) βˆ– I ) ∧ βˆ€π‘ ∈ (0..^π‘Ž) Β¬ 𝑒 ∈ dom ((π‘€β€˜π‘) βˆ– I ))) ↔ βˆƒπ‘₯ ∈ Word 𝑇(((𝐺 Ξ£g π‘₯) = ( I β†Ύ 𝐷) ∧ (β™―β€˜π‘₯) = 𝐿) ∧ (𝑏 ∈ (0..^𝐿) ∧ 𝑒 ∈ dom ((π‘₯β€˜π‘) βˆ– I ) ∧ βˆ€π‘‘ ∈ (0..^𝑏) Β¬ 𝑒 ∈ dom ((π‘₯β€˜π‘‘) βˆ– I )))))
7372imbi2d 341 . . . . . 6 (π‘Ž = 𝑏 β†’ (((πœ‘ ∧ 𝑒 ∈ dom ((π‘Šβ€˜0) βˆ– I )) β†’ βˆƒπ‘€ ∈ Word 𝑇(((𝐺 Ξ£g 𝑀) = ( I β†Ύ 𝐷) ∧ (β™―β€˜π‘€) = 𝐿) ∧ (π‘Ž ∈ (0..^𝐿) ∧ 𝑒 ∈ dom ((π‘€β€˜π‘Ž) βˆ– I ) ∧ βˆ€π‘ ∈ (0..^π‘Ž) Β¬ 𝑒 ∈ dom ((π‘€β€˜π‘) βˆ– I )))) ↔ ((πœ‘ ∧ 𝑒 ∈ dom ((π‘Šβ€˜0) βˆ– I )) β†’ βˆƒπ‘₯ ∈ Word 𝑇(((𝐺 Ξ£g π‘₯) = ( I β†Ύ 𝐷) ∧ (β™―β€˜π‘₯) = 𝐿) ∧ (𝑏 ∈ (0..^𝐿) ∧ 𝑒 ∈ dom ((π‘₯β€˜π‘) βˆ– I ) ∧ βˆ€π‘‘ ∈ (0..^𝑏) Β¬ 𝑒 ∈ dom ((π‘₯β€˜π‘‘) βˆ– I ))))))
74 eleq1 2826 . . . . . . . . . 10 (π‘Ž = (𝑏 + 1) β†’ (π‘Ž ∈ (0..^𝐿) ↔ (𝑏 + 1) ∈ (0..^𝐿)))
75 fveq2 6847 . . . . . . . . . . . . 13 (π‘Ž = (𝑏 + 1) β†’ (π‘€β€˜π‘Ž) = (π‘€β€˜(𝑏 + 1)))
7675difeq1d 4086 . . . . . . . . . . . 12 (π‘Ž = (𝑏 + 1) β†’ ((π‘€β€˜π‘Ž) βˆ– I ) = ((π‘€β€˜(𝑏 + 1)) βˆ– I ))
7776dmeqd 5866 . . . . . . . . . . 11 (π‘Ž = (𝑏 + 1) β†’ dom ((π‘€β€˜π‘Ž) βˆ– I ) = dom ((π‘€β€˜(𝑏 + 1)) βˆ– I ))
7877eleq2d 2824 . . . . . . . . . 10 (π‘Ž = (𝑏 + 1) β†’ (𝑒 ∈ dom ((π‘€β€˜π‘Ž) βˆ– I ) ↔ 𝑒 ∈ dom ((π‘€β€˜(𝑏 + 1)) βˆ– I )))
79 oveq2 7370 . . . . . . . . . . 11 (π‘Ž = (𝑏 + 1) β†’ (0..^π‘Ž) = (0..^(𝑏 + 1)))
8079raleqdv 3316 . . . . . . . . . 10 (π‘Ž = (𝑏 + 1) β†’ (βˆ€π‘ ∈ (0..^π‘Ž) Β¬ 𝑒 ∈ dom ((π‘€β€˜π‘) βˆ– I ) ↔ βˆ€π‘ ∈ (0..^(𝑏 + 1)) Β¬ 𝑒 ∈ dom ((π‘€β€˜π‘) βˆ– I )))
8174, 78, 803anbi123d 1437 . . . . . . . . 9 (π‘Ž = (𝑏 + 1) β†’ ((π‘Ž ∈ (0..^𝐿) ∧ 𝑒 ∈ dom ((π‘€β€˜π‘Ž) βˆ– I ) ∧ βˆ€π‘ ∈ (0..^π‘Ž) Β¬ 𝑒 ∈ dom ((π‘€β€˜π‘) βˆ– I )) ↔ ((𝑏 + 1) ∈ (0..^𝐿) ∧ 𝑒 ∈ dom ((π‘€β€˜(𝑏 + 1)) βˆ– I ) ∧ βˆ€π‘ ∈ (0..^(𝑏 + 1)) Β¬ 𝑒 ∈ dom ((π‘€β€˜π‘) βˆ– I ))))
8281anbi2d 630 . . . . . . . 8 (π‘Ž = (𝑏 + 1) β†’ ((((𝐺 Ξ£g 𝑀) = ( I β†Ύ 𝐷) ∧ (β™―β€˜π‘€) = 𝐿) ∧ (π‘Ž ∈ (0..^𝐿) ∧ 𝑒 ∈ dom ((π‘€β€˜π‘Ž) βˆ– I ) ∧ βˆ€π‘ ∈ (0..^π‘Ž) Β¬ 𝑒 ∈ dom ((π‘€β€˜π‘) βˆ– I ))) ↔ (((𝐺 Ξ£g 𝑀) = ( I β†Ύ 𝐷) ∧ (β™―β€˜π‘€) = 𝐿) ∧ ((𝑏 + 1) ∈ (0..^𝐿) ∧ 𝑒 ∈ dom ((π‘€β€˜(𝑏 + 1)) βˆ– I ) ∧ βˆ€π‘ ∈ (0..^(𝑏 + 1)) Β¬ 𝑒 ∈ dom ((π‘€β€˜π‘) βˆ– I )))))
8382rexbidv 3176 . . . . . . 7 (π‘Ž = (𝑏 + 1) β†’ (βˆƒπ‘€ ∈ Word 𝑇(((𝐺 Ξ£g 𝑀) = ( I β†Ύ 𝐷) ∧ (β™―β€˜π‘€) = 𝐿) ∧ (π‘Ž ∈ (0..^𝐿) ∧ 𝑒 ∈ dom ((π‘€β€˜π‘Ž) βˆ– I ) ∧ βˆ€π‘ ∈ (0..^π‘Ž) Β¬ 𝑒 ∈ dom ((π‘€β€˜π‘) βˆ– I ))) ↔ βˆƒπ‘€ ∈ Word 𝑇(((𝐺 Ξ£g 𝑀) = ( I β†Ύ 𝐷) ∧ (β™―β€˜π‘€) = 𝐿) ∧ ((𝑏 + 1) ∈ (0..^𝐿) ∧ 𝑒 ∈ dom ((π‘€β€˜(𝑏 + 1)) βˆ– I ) ∧ βˆ€π‘ ∈ (0..^(𝑏 + 1)) Β¬ 𝑒 ∈ dom ((π‘€β€˜π‘) βˆ– I )))))
8483imbi2d 341 . . . . . 6 (π‘Ž = (𝑏 + 1) β†’ (((πœ‘ ∧ 𝑒 ∈ dom ((π‘Šβ€˜0) βˆ– I )) β†’ βˆƒπ‘€ ∈ Word 𝑇(((𝐺 Ξ£g 𝑀) = ( I β†Ύ 𝐷) ∧ (β™―β€˜π‘€) = 𝐿) ∧ (π‘Ž ∈ (0..^𝐿) ∧ 𝑒 ∈ dom ((π‘€β€˜π‘Ž) βˆ– I ) ∧ βˆ€π‘ ∈ (0..^π‘Ž) Β¬ 𝑒 ∈ dom ((π‘€β€˜π‘) βˆ– I )))) ↔ ((πœ‘ ∧ 𝑒 ∈ dom ((π‘Šβ€˜0) βˆ– I )) β†’ βˆƒπ‘€ ∈ Word 𝑇(((𝐺 Ξ£g 𝑀) = ( I β†Ύ 𝐷) ∧ (β™―β€˜π‘€) = 𝐿) ∧ ((𝑏 + 1) ∈ (0..^𝐿) ∧ 𝑒 ∈ dom ((π‘€β€˜(𝑏 + 1)) βˆ– I ) ∧ βˆ€π‘ ∈ (0..^(𝑏 + 1)) Β¬ 𝑒 ∈ dom ((π‘€β€˜π‘) βˆ– I ))))))
85 eleq1 2826 . . . . . . . . . 10 (π‘Ž = 𝐿 β†’ (π‘Ž ∈ (0..^𝐿) ↔ 𝐿 ∈ (0..^𝐿)))
86 fveq2 6847 . . . . . . . . . . . . 13 (π‘Ž = 𝐿 β†’ (π‘€β€˜π‘Ž) = (π‘€β€˜πΏ))
8786difeq1d 4086 . . . . . . . . . . . 12 (π‘Ž = 𝐿 β†’ ((π‘€β€˜π‘Ž) βˆ– I ) = ((π‘€β€˜πΏ) βˆ– I ))
8887dmeqd 5866 . . . . . . . . . . 11 (π‘Ž = 𝐿 β†’ dom ((π‘€β€˜π‘Ž) βˆ– I ) = dom ((π‘€β€˜πΏ) βˆ– I ))
8988eleq2d 2824 . . . . . . . . . 10 (π‘Ž = 𝐿 β†’ (𝑒 ∈ dom ((π‘€β€˜π‘Ž) βˆ– I ) ↔ 𝑒 ∈ dom ((π‘€β€˜πΏ) βˆ– I )))
90 oveq2 7370 . . . . . . . . . . 11 (π‘Ž = 𝐿 β†’ (0..^π‘Ž) = (0..^𝐿))
9190raleqdv 3316 . . . . . . . . . 10 (π‘Ž = 𝐿 β†’ (βˆ€π‘ ∈ (0..^π‘Ž) Β¬ 𝑒 ∈ dom ((π‘€β€˜π‘) βˆ– I ) ↔ βˆ€π‘ ∈ (0..^𝐿) Β¬ 𝑒 ∈ dom ((π‘€β€˜π‘) βˆ– I )))
9285, 89, 913anbi123d 1437 . . . . . . . . 9 (π‘Ž = 𝐿 β†’ ((π‘Ž ∈ (0..^𝐿) ∧ 𝑒 ∈ dom ((π‘€β€˜π‘Ž) βˆ– I ) ∧ βˆ€π‘ ∈ (0..^π‘Ž) Β¬ 𝑒 ∈ dom ((π‘€β€˜π‘) βˆ– I )) ↔ (𝐿 ∈ (0..^𝐿) ∧ 𝑒 ∈ dom ((π‘€β€˜πΏ) βˆ– I ) ∧ βˆ€π‘ ∈ (0..^𝐿) Β¬ 𝑒 ∈ dom ((π‘€β€˜π‘) βˆ– I ))))
9392anbi2d 630 . . . . . . . 8 (π‘Ž = 𝐿 β†’ ((((𝐺 Ξ£g 𝑀) = ( I β†Ύ 𝐷) ∧ (β™―β€˜π‘€) = 𝐿) ∧ (π‘Ž ∈ (0..^𝐿) ∧ 𝑒 ∈ dom ((π‘€β€˜π‘Ž) βˆ– I ) ∧ βˆ€π‘ ∈ (0..^π‘Ž) Β¬ 𝑒 ∈ dom ((π‘€β€˜π‘) βˆ– I ))) ↔ (((𝐺 Ξ£g 𝑀) = ( I β†Ύ 𝐷) ∧ (β™―β€˜π‘€) = 𝐿) ∧ (𝐿 ∈ (0..^𝐿) ∧ 𝑒 ∈ dom ((π‘€β€˜πΏ) βˆ– I ) ∧ βˆ€π‘ ∈ (0..^𝐿) Β¬ 𝑒 ∈ dom ((π‘€β€˜π‘) βˆ– I )))))
9493rexbidv 3176 . . . . . . 7 (π‘Ž = 𝐿 β†’ (βˆƒπ‘€ ∈ Word 𝑇(((𝐺 Ξ£g 𝑀) = ( I β†Ύ 𝐷) ∧ (β™―β€˜π‘€) = 𝐿) ∧ (π‘Ž ∈ (0..^𝐿) ∧ 𝑒 ∈ dom ((π‘€β€˜π‘Ž) βˆ– I ) ∧ βˆ€π‘ ∈ (0..^π‘Ž) Β¬ 𝑒 ∈ dom ((π‘€β€˜π‘) βˆ– I ))) ↔ βˆƒπ‘€ ∈ Word 𝑇(((𝐺 Ξ£g 𝑀) = ( I β†Ύ 𝐷) ∧ (β™―β€˜π‘€) = 𝐿) ∧ (𝐿 ∈ (0..^𝐿) ∧ 𝑒 ∈ dom ((π‘€β€˜πΏ) βˆ– I ) ∧ βˆ€π‘ ∈ (0..^𝐿) Β¬ 𝑒 ∈ dom ((π‘€β€˜π‘) βˆ– I )))))
9594imbi2d 341 . . . . . 6 (π‘Ž = 𝐿 β†’ (((πœ‘ ∧ 𝑒 ∈ dom ((π‘Šβ€˜0) βˆ– I )) β†’ βˆƒπ‘€ ∈ Word 𝑇(((𝐺 Ξ£g 𝑀) = ( I β†Ύ 𝐷) ∧ (β™―β€˜π‘€) = 𝐿) ∧ (π‘Ž ∈ (0..^𝐿) ∧ 𝑒 ∈ dom ((π‘€β€˜π‘Ž) βˆ– I ) ∧ βˆ€π‘ ∈ (0..^π‘Ž) Β¬ 𝑒 ∈ dom ((π‘€β€˜π‘) βˆ– I )))) ↔ ((πœ‘ ∧ 𝑒 ∈ dom ((π‘Šβ€˜0) βˆ– I )) β†’ βˆƒπ‘€ ∈ Word 𝑇(((𝐺 Ξ£g 𝑀) = ( I β†Ύ 𝐷) ∧ (β™―β€˜π‘€) = 𝐿) ∧ (𝐿 ∈ (0..^𝐿) ∧ 𝑒 ∈ dom ((π‘€β€˜πΏ) βˆ– I ) ∧ βˆ€π‘ ∈ (0..^𝐿) Β¬ 𝑒 ∈ dom ((π‘€β€˜π‘) βˆ– I ))))))
965adantr 482 . . . . . . 7 ((πœ‘ ∧ 𝑒 ∈ dom ((π‘Šβ€˜0) βˆ– I )) β†’ π‘Š ∈ Word 𝑇)
97 psgnunilem3.w3 . . . . . . . . 9 (πœ‘ β†’ (𝐺 Ξ£g π‘Š) = ( I β†Ύ 𝐷))
9897, 1jca 513 . . . . . . . 8 (πœ‘ β†’ ((𝐺 Ξ£g π‘Š) = ( I β†Ύ 𝐷) ∧ (β™―β€˜π‘Š) = 𝐿))
9998adantr 482 . . . . . . 7 ((πœ‘ ∧ 𝑒 ∈ dom ((π‘Šβ€˜0) βˆ– I )) β†’ ((𝐺 Ξ£g π‘Š) = ( I β†Ύ 𝐷) ∧ (β™―β€˜π‘Š) = 𝐿))
10012adantr 482 . . . . . . . 8 ((πœ‘ ∧ 𝑒 ∈ dom ((π‘Šβ€˜0) βˆ– I )) β†’ 0 ∈ (0..^𝐿))
101 simpr 486 . . . . . . . 8 ((πœ‘ ∧ 𝑒 ∈ dom ((π‘Šβ€˜0) βˆ– I )) β†’ 𝑒 ∈ dom ((π‘Šβ€˜0) βˆ– I ))
102 ral0 4475 . . . . . . . . . 10 βˆ€π‘ ∈ βˆ… Β¬ 𝑒 ∈ dom ((π‘Šβ€˜π‘) βˆ– I )
103 fzo0 13603 . . . . . . . . . . 11 (0..^0) = βˆ…
104103raleqi 3314 . . . . . . . . . 10 (βˆ€π‘ ∈ (0..^0) Β¬ 𝑒 ∈ dom ((π‘Šβ€˜π‘) βˆ– I ) ↔ βˆ€π‘ ∈ βˆ… Β¬ 𝑒 ∈ dom ((π‘Šβ€˜π‘) βˆ– I ))
105102, 104mpbir 230 . . . . . . . . 9 βˆ€π‘ ∈ (0..^0) Β¬ 𝑒 ∈ dom ((π‘Šβ€˜π‘) βˆ– I )
106105a1i 11 . . . . . . . 8 ((πœ‘ ∧ 𝑒 ∈ dom ((π‘Šβ€˜0) βˆ– I )) β†’ βˆ€π‘ ∈ (0..^0) Β¬ 𝑒 ∈ dom ((π‘Šβ€˜π‘) βˆ– I ))
107100, 101, 1063jca 1129 . . . . . . 7 ((πœ‘ ∧ 𝑒 ∈ dom ((π‘Šβ€˜0) βˆ– I )) β†’ (0 ∈ (0..^𝐿) ∧ 𝑒 ∈ dom ((π‘Šβ€˜0) βˆ– I ) ∧ βˆ€π‘ ∈ (0..^0) Β¬ 𝑒 ∈ dom ((π‘Šβ€˜π‘) βˆ– I )))
108 oveq2 7370 . . . . . . . . . . 11 (𝑀 = π‘Š β†’ (𝐺 Ξ£g 𝑀) = (𝐺 Ξ£g π‘Š))
109108eqeq1d 2739 . . . . . . . . . 10 (𝑀 = π‘Š β†’ ((𝐺 Ξ£g 𝑀) = ( I β†Ύ 𝐷) ↔ (𝐺 Ξ£g π‘Š) = ( I β†Ύ 𝐷)))
110 fveqeq2 6856 . . . . . . . . . 10 (𝑀 = π‘Š β†’ ((β™―β€˜π‘€) = 𝐿 ↔ (β™―β€˜π‘Š) = 𝐿))
111109, 110anbi12d 632 . . . . . . . . 9 (𝑀 = π‘Š β†’ (((𝐺 Ξ£g 𝑀) = ( I β†Ύ 𝐷) ∧ (β™―β€˜π‘€) = 𝐿) ↔ ((𝐺 Ξ£g π‘Š) = ( I β†Ύ 𝐷) ∧ (β™―β€˜π‘Š) = 𝐿)))
112 fveq1 6846 . . . . . . . . . . . . 13 (𝑀 = π‘Š β†’ (π‘€β€˜0) = (π‘Šβ€˜0))
113112difeq1d 4086 . . . . . . . . . . . 12 (𝑀 = π‘Š β†’ ((π‘€β€˜0) βˆ– I ) = ((π‘Šβ€˜0) βˆ– I ))
114113dmeqd 5866 . . . . . . . . . . 11 (𝑀 = π‘Š β†’ dom ((π‘€β€˜0) βˆ– I ) = dom ((π‘Šβ€˜0) βˆ– I ))
115114eleq2d 2824 . . . . . . . . . 10 (𝑀 = π‘Š β†’ (𝑒 ∈ dom ((π‘€β€˜0) βˆ– I ) ↔ 𝑒 ∈ dom ((π‘Šβ€˜0) βˆ– I )))
116 fveq1 6846 . . . . . . . . . . . . . . 15 (𝑀 = π‘Š β†’ (π‘€β€˜π‘) = (π‘Šβ€˜π‘))
117116difeq1d 4086 . . . . . . . . . . . . . 14 (𝑀 = π‘Š β†’ ((π‘€β€˜π‘) βˆ– I ) = ((π‘Šβ€˜π‘) βˆ– I ))
118117dmeqd 5866 . . . . . . . . . . . . 13 (𝑀 = π‘Š β†’ dom ((π‘€β€˜π‘) βˆ– I ) = dom ((π‘Šβ€˜π‘) βˆ– I ))
119118eleq2d 2824 . . . . . . . . . . . 12 (𝑀 = π‘Š β†’ (𝑒 ∈ dom ((π‘€β€˜π‘) βˆ– I ) ↔ 𝑒 ∈ dom ((π‘Šβ€˜π‘) βˆ– I )))
120119notbid 318 . . . . . . . . . . 11 (𝑀 = π‘Š β†’ (Β¬ 𝑒 ∈ dom ((π‘€β€˜π‘) βˆ– I ) ↔ Β¬ 𝑒 ∈ dom ((π‘Šβ€˜π‘) βˆ– I )))
121120ralbidv 3175 . . . . . . . . . 10 (𝑀 = π‘Š β†’ (βˆ€π‘ ∈ (0..^0) Β¬ 𝑒 ∈ dom ((π‘€β€˜π‘) βˆ– I ) ↔ βˆ€π‘ ∈ (0..^0) Β¬ 𝑒 ∈ dom ((π‘Šβ€˜π‘) βˆ– I )))
122115, 1213anbi23d 1440 . . . . . . . . 9 (𝑀 = π‘Š β†’ ((0 ∈ (0..^𝐿) ∧ 𝑒 ∈ dom ((π‘€β€˜0) βˆ– I ) ∧ βˆ€π‘ ∈ (0..^0) Β¬ 𝑒 ∈ dom ((π‘€β€˜π‘) βˆ– I )) ↔ (0 ∈ (0..^𝐿) ∧ 𝑒 ∈ dom ((π‘Šβ€˜0) βˆ– I ) ∧ βˆ€π‘ ∈ (0..^0) Β¬ 𝑒 ∈ dom ((π‘Šβ€˜π‘) βˆ– I ))))
123111, 122anbi12d 632 . . . . . . . 8 (𝑀 = π‘Š β†’ ((((𝐺 Ξ£g 𝑀) = ( I β†Ύ 𝐷) ∧ (β™―β€˜π‘€) = 𝐿) ∧ (0 ∈ (0..^𝐿) ∧ 𝑒 ∈ dom ((π‘€β€˜0) βˆ– I ) ∧ βˆ€π‘ ∈ (0..^0) Β¬ 𝑒 ∈ dom ((π‘€β€˜π‘) βˆ– I ))) ↔ (((𝐺 Ξ£g π‘Š) = ( I β†Ύ 𝐷) ∧ (β™―β€˜π‘Š) = 𝐿) ∧ (0 ∈ (0..^𝐿) ∧ 𝑒 ∈ dom ((π‘Šβ€˜0) βˆ– I ) ∧ βˆ€π‘ ∈ (0..^0) Β¬ 𝑒 ∈ dom ((π‘Šβ€˜π‘) βˆ– I )))))
124123rspcev 3584 . . . . . . 7 ((π‘Š ∈ Word 𝑇 ∧ (((𝐺 Ξ£g π‘Š) = ( I β†Ύ 𝐷) ∧ (β™―β€˜π‘Š) = 𝐿) ∧ (0 ∈ (0..^𝐿) ∧ 𝑒 ∈ dom ((π‘Šβ€˜0) βˆ– I ) ∧ βˆ€π‘ ∈ (0..^0) Β¬ 𝑒 ∈ dom ((π‘Šβ€˜π‘) βˆ– I )))) β†’ βˆƒπ‘€ ∈ Word 𝑇(((𝐺 Ξ£g 𝑀) = ( I β†Ύ 𝐷) ∧ (β™―β€˜π‘€) = 𝐿) ∧ (0 ∈ (0..^𝐿) ∧ 𝑒 ∈ dom ((π‘€β€˜0) βˆ– I ) ∧ βˆ€π‘ ∈ (0..^0) Β¬ 𝑒 ∈ dom ((π‘€β€˜π‘) βˆ– I ))))
12596, 99, 107, 124syl12anc 836 . . . . . 6 ((πœ‘ ∧ 𝑒 ∈ dom ((π‘Šβ€˜0) βˆ– I )) β†’ βˆƒπ‘€ ∈ Word 𝑇(((𝐺 Ξ£g 𝑀) = ( I β†Ύ 𝐷) ∧ (β™―β€˜π‘€) = 𝐿) ∧ (0 ∈ (0..^𝐿) ∧ 𝑒 ∈ dom ((π‘€β€˜0) βˆ– I ) ∧ βˆ€π‘ ∈ (0..^0) Β¬ 𝑒 ∈ dom ((π‘€β€˜π‘) βˆ– I ))))
126 psgnunilem3.g . . . . . . . . . 10 𝐺 = (SymGrpβ€˜π·)
127 psgnunilem3.d . . . . . . . . . . 11 (πœ‘ β†’ 𝐷 ∈ 𝑉)
128127ad2antrr 725 . . . . . . . . . 10 (((πœ‘ ∧ 𝑒 ∈ dom ((π‘Šβ€˜0) βˆ– I )) ∧ (π‘₯ ∈ Word 𝑇 ∧ (((𝐺 Ξ£g π‘₯) = ( I β†Ύ 𝐷) ∧ (β™―β€˜π‘₯) = 𝐿) ∧ (𝑏 ∈ (0..^𝐿) ∧ 𝑒 ∈ dom ((π‘₯β€˜π‘) βˆ– I ) ∧ βˆ€π‘‘ ∈ (0..^𝑏) Β¬ 𝑒 ∈ dom ((π‘₯β€˜π‘‘) βˆ– I ))))) β†’ 𝐷 ∈ 𝑉)
129 simprl 770 . . . . . . . . . 10 (((πœ‘ ∧ 𝑒 ∈ dom ((π‘Šβ€˜0) βˆ– I )) ∧ (π‘₯ ∈ Word 𝑇 ∧ (((𝐺 Ξ£g π‘₯) = ( I β†Ύ 𝐷) ∧ (β™―β€˜π‘₯) = 𝐿) ∧ (𝑏 ∈ (0..^𝐿) ∧ 𝑒 ∈ dom ((π‘₯β€˜π‘) βˆ– I ) ∧ βˆ€π‘‘ ∈ (0..^𝑏) Β¬ 𝑒 ∈ dom ((π‘₯β€˜π‘‘) βˆ– I ))))) β†’ π‘₯ ∈ Word 𝑇)
130 simpll 766 . . . . . . . . . . 11 ((((𝐺 Ξ£g π‘₯) = ( I β†Ύ 𝐷) ∧ (β™―β€˜π‘₯) = 𝐿) ∧ (𝑏 ∈ (0..^𝐿) ∧ 𝑒 ∈ dom ((π‘₯β€˜π‘) βˆ– I ) ∧ βˆ€π‘‘ ∈ (0..^𝑏) Β¬ 𝑒 ∈ dom ((π‘₯β€˜π‘‘) βˆ– I ))) β†’ (𝐺 Ξ£g π‘₯) = ( I β†Ύ 𝐷))
131130ad2antll 728 . . . . . . . . . 10 (((πœ‘ ∧ 𝑒 ∈ dom ((π‘Šβ€˜0) βˆ– I )) ∧ (π‘₯ ∈ Word 𝑇 ∧ (((𝐺 Ξ£g π‘₯) = ( I β†Ύ 𝐷) ∧ (β™―β€˜π‘₯) = 𝐿) ∧ (𝑏 ∈ (0..^𝐿) ∧ 𝑒 ∈ dom ((π‘₯β€˜π‘) βˆ– I ) ∧ βˆ€π‘‘ ∈ (0..^𝑏) Β¬ 𝑒 ∈ dom ((π‘₯β€˜π‘‘) βˆ– I ))))) β†’ (𝐺 Ξ£g π‘₯) = ( I β†Ύ 𝐷))
132 simplr 768 . . . . . . . . . . 11 ((((𝐺 Ξ£g π‘₯) = ( I β†Ύ 𝐷) ∧ (β™―β€˜π‘₯) = 𝐿) ∧ (𝑏 ∈ (0..^𝐿) ∧ 𝑒 ∈ dom ((π‘₯β€˜π‘) βˆ– I ) ∧ βˆ€π‘‘ ∈ (0..^𝑏) Β¬ 𝑒 ∈ dom ((π‘₯β€˜π‘‘) βˆ– I ))) β†’ (β™―β€˜π‘₯) = 𝐿)
133132ad2antll 728 . . . . . . . . . 10 (((πœ‘ ∧ 𝑒 ∈ dom ((π‘Šβ€˜0) βˆ– I )) ∧ (π‘₯ ∈ Word 𝑇 ∧ (((𝐺 Ξ£g π‘₯) = ( I β†Ύ 𝐷) ∧ (β™―β€˜π‘₯) = 𝐿) ∧ (𝑏 ∈ (0..^𝐿) ∧ 𝑒 ∈ dom ((π‘₯β€˜π‘) βˆ– I ) ∧ βˆ€π‘‘ ∈ (0..^𝑏) Β¬ 𝑒 ∈ dom ((π‘₯β€˜π‘‘) βˆ– I ))))) β†’ (β™―β€˜π‘₯) = 𝐿)
134 simpr1 1195 . . . . . . . . . . 11 ((((𝐺 Ξ£g π‘₯) = ( I β†Ύ 𝐷) ∧ (β™―β€˜π‘₯) = 𝐿) ∧ (𝑏 ∈ (0..^𝐿) ∧ 𝑒 ∈ dom ((π‘₯β€˜π‘) βˆ– I ) ∧ βˆ€π‘‘ ∈ (0..^𝑏) Β¬ 𝑒 ∈ dom ((π‘₯β€˜π‘‘) βˆ– I ))) β†’ 𝑏 ∈ (0..^𝐿))
135134ad2antll 728 . . . . . . . . . 10 (((πœ‘ ∧ 𝑒 ∈ dom ((π‘Šβ€˜0) βˆ– I )) ∧ (π‘₯ ∈ Word 𝑇 ∧ (((𝐺 Ξ£g π‘₯) = ( I β†Ύ 𝐷) ∧ (β™―β€˜π‘₯) = 𝐿) ∧ (𝑏 ∈ (0..^𝐿) ∧ 𝑒 ∈ dom ((π‘₯β€˜π‘) βˆ– I ) ∧ βˆ€π‘‘ ∈ (0..^𝑏) Β¬ 𝑒 ∈ dom ((π‘₯β€˜π‘‘) βˆ– I ))))) β†’ 𝑏 ∈ (0..^𝐿))
136 simpr2 1196 . . . . . . . . . . 11 ((((𝐺 Ξ£g π‘₯) = ( I β†Ύ 𝐷) ∧ (β™―β€˜π‘₯) = 𝐿) ∧ (𝑏 ∈ (0..^𝐿) ∧ 𝑒 ∈ dom ((π‘₯β€˜π‘) βˆ– I ) ∧ βˆ€π‘‘ ∈ (0..^𝑏) Β¬ 𝑒 ∈ dom ((π‘₯β€˜π‘‘) βˆ– I ))) β†’ 𝑒 ∈ dom ((π‘₯β€˜π‘) βˆ– I ))
137136ad2antll 728 . . . . . . . . . 10 (((πœ‘ ∧ 𝑒 ∈ dom ((π‘Šβ€˜0) βˆ– I )) ∧ (π‘₯ ∈ Word 𝑇 ∧ (((𝐺 Ξ£g π‘₯) = ( I β†Ύ 𝐷) ∧ (β™―β€˜π‘₯) = 𝐿) ∧ (𝑏 ∈ (0..^𝐿) ∧ 𝑒 ∈ dom ((π‘₯β€˜π‘) βˆ– I ) ∧ βˆ€π‘‘ ∈ (0..^𝑏) Β¬ 𝑒 ∈ dom ((π‘₯β€˜π‘‘) βˆ– I ))))) β†’ 𝑒 ∈ dom ((π‘₯β€˜π‘) βˆ– I ))
138 simpr3 1197 . . . . . . . . . . 11 ((((𝐺 Ξ£g π‘₯) = ( I β†Ύ 𝐷) ∧ (β™―β€˜π‘₯) = 𝐿) ∧ (𝑏 ∈ (0..^𝐿) ∧ 𝑒 ∈ dom ((π‘₯β€˜π‘) βˆ– I ) ∧ βˆ€π‘‘ ∈ (0..^𝑏) Β¬ 𝑒 ∈ dom ((π‘₯β€˜π‘‘) βˆ– I ))) β†’ βˆ€π‘‘ ∈ (0..^𝑏) Β¬ 𝑒 ∈ dom ((π‘₯β€˜π‘‘) βˆ– I ))
139138ad2antll 728 . . . . . . . . . 10 (((πœ‘ ∧ 𝑒 ∈ dom ((π‘Šβ€˜0) βˆ– I )) ∧ (π‘₯ ∈ Word 𝑇 ∧ (((𝐺 Ξ£g π‘₯) = ( I β†Ύ 𝐷) ∧ (β™―β€˜π‘₯) = 𝐿) ∧ (𝑏 ∈ (0..^𝐿) ∧ 𝑒 ∈ dom ((π‘₯β€˜π‘) βˆ– I ) ∧ βˆ€π‘‘ ∈ (0..^𝑏) Β¬ 𝑒 ∈ dom ((π‘₯β€˜π‘‘) βˆ– I ))))) β†’ βˆ€π‘‘ ∈ (0..^𝑏) Β¬ 𝑒 ∈ dom ((π‘₯β€˜π‘‘) βˆ– I ))
140 psgnunilem3.in . . . . . . . . . . . 12 (πœ‘ β†’ Β¬ βˆƒπ‘₯ ∈ Word 𝑇((β™―β€˜π‘₯) = (𝐿 βˆ’ 2) ∧ (𝐺 Ξ£g π‘₯) = ( I β†Ύ 𝐷)))
141 fveqeq2 6856 . . . . . . . . . . . . . 14 (π‘₯ = 𝑦 β†’ ((β™―β€˜π‘₯) = (𝐿 βˆ’ 2) ↔ (β™―β€˜π‘¦) = (𝐿 βˆ’ 2)))
142 oveq2 7370 . . . . . . . . . . . . . . 15 (π‘₯ = 𝑦 β†’ (𝐺 Ξ£g π‘₯) = (𝐺 Ξ£g 𝑦))
143142eqeq1d 2739 . . . . . . . . . . . . . 14 (π‘₯ = 𝑦 β†’ ((𝐺 Ξ£g π‘₯) = ( I β†Ύ 𝐷) ↔ (𝐺 Ξ£g 𝑦) = ( I β†Ύ 𝐷)))
144141, 143anbi12d 632 . . . . . . . . . . . . 13 (π‘₯ = 𝑦 β†’ (((β™―β€˜π‘₯) = (𝐿 βˆ’ 2) ∧ (𝐺 Ξ£g π‘₯) = ( I β†Ύ 𝐷)) ↔ ((β™―β€˜π‘¦) = (𝐿 βˆ’ 2) ∧ (𝐺 Ξ£g 𝑦) = ( I β†Ύ 𝐷))))
145144cbvrexvw 3229 . . . . . . . . . . . 12 (βˆƒπ‘₯ ∈ Word 𝑇((β™―β€˜π‘₯) = (𝐿 βˆ’ 2) ∧ (𝐺 Ξ£g π‘₯) = ( I β†Ύ 𝐷)) ↔ βˆƒπ‘¦ ∈ Word 𝑇((β™―β€˜π‘¦) = (𝐿 βˆ’ 2) ∧ (𝐺 Ξ£g 𝑦) = ( I β†Ύ 𝐷)))
146140, 145sylnib 328 . . . . . . . . . . 11 (πœ‘ β†’ Β¬ βˆƒπ‘¦ ∈ Word 𝑇((β™―β€˜π‘¦) = (𝐿 βˆ’ 2) ∧ (𝐺 Ξ£g 𝑦) = ( I β†Ύ 𝐷)))
147146ad2antrr 725 . . . . . . . . . 10 (((πœ‘ ∧ 𝑒 ∈ dom ((π‘Šβ€˜0) βˆ– I )) ∧ (π‘₯ ∈ Word 𝑇 ∧ (((𝐺 Ξ£g π‘₯) = ( I β†Ύ 𝐷) ∧ (β™―β€˜π‘₯) = 𝐿) ∧ (𝑏 ∈ (0..^𝐿) ∧ 𝑒 ∈ dom ((π‘₯β€˜π‘) βˆ– I ) ∧ βˆ€π‘‘ ∈ (0..^𝑏) Β¬ 𝑒 ∈ dom ((π‘₯β€˜π‘‘) βˆ– I ))))) β†’ Β¬ βˆƒπ‘¦ ∈ Word 𝑇((β™―β€˜π‘¦) = (𝐿 βˆ’ 2) ∧ (𝐺 Ξ£g 𝑦) = ( I β†Ύ 𝐷)))
148126, 17, 128, 129, 131, 133, 135, 137, 139, 147psgnunilem2 19284 . . . . . . . . 9 (((πœ‘ ∧ 𝑒 ∈ dom ((π‘Šβ€˜0) βˆ– I )) ∧ (π‘₯ ∈ Word 𝑇 ∧ (((𝐺 Ξ£g π‘₯) = ( I β†Ύ 𝐷) ∧ (β™―β€˜π‘₯) = 𝐿) ∧ (𝑏 ∈ (0..^𝐿) ∧ 𝑒 ∈ dom ((π‘₯β€˜π‘) βˆ– I ) ∧ βˆ€π‘‘ ∈ (0..^𝑏) Β¬ 𝑒 ∈ dom ((π‘₯β€˜π‘‘) βˆ– I ))))) β†’ βˆƒπ‘€ ∈ Word 𝑇(((𝐺 Ξ£g 𝑀) = ( I β†Ύ 𝐷) ∧ (β™―β€˜π‘€) = 𝐿) ∧ ((𝑏 + 1) ∈ (0..^𝐿) ∧ 𝑒 ∈ dom ((π‘€β€˜(𝑏 + 1)) βˆ– I ) ∧ βˆ€π‘ ∈ (0..^(𝑏 + 1)) Β¬ 𝑒 ∈ dom ((π‘€β€˜π‘) βˆ– I ))))
149148rexlimdvaa 3154 . . . . . . . 8 ((πœ‘ ∧ 𝑒 ∈ dom ((π‘Šβ€˜0) βˆ– I )) β†’ (βˆƒπ‘₯ ∈ Word 𝑇(((𝐺 Ξ£g π‘₯) = ( I β†Ύ 𝐷) ∧ (β™―β€˜π‘₯) = 𝐿) ∧ (𝑏 ∈ (0..^𝐿) ∧ 𝑒 ∈ dom ((π‘₯β€˜π‘) βˆ– I ) ∧ βˆ€π‘‘ ∈ (0..^𝑏) Β¬ 𝑒 ∈ dom ((π‘₯β€˜π‘‘) βˆ– I ))) β†’ βˆƒπ‘€ ∈ Word 𝑇(((𝐺 Ξ£g 𝑀) = ( I β†Ύ 𝐷) ∧ (β™―β€˜π‘€) = 𝐿) ∧ ((𝑏 + 1) ∈ (0..^𝐿) ∧ 𝑒 ∈ dom ((π‘€β€˜(𝑏 + 1)) βˆ– I ) ∧ βˆ€π‘ ∈ (0..^(𝑏 + 1)) Β¬ 𝑒 ∈ dom ((π‘€β€˜π‘) βˆ– I )))))
150149a2i 14 . . . . . . 7 (((πœ‘ ∧ 𝑒 ∈ dom ((π‘Šβ€˜0) βˆ– I )) β†’ βˆƒπ‘₯ ∈ Word 𝑇(((𝐺 Ξ£g π‘₯) = ( I β†Ύ 𝐷) ∧ (β™―β€˜π‘₯) = 𝐿) ∧ (𝑏 ∈ (0..^𝐿) ∧ 𝑒 ∈ dom ((π‘₯β€˜π‘) βˆ– I ) ∧ βˆ€π‘‘ ∈ (0..^𝑏) Β¬ 𝑒 ∈ dom ((π‘₯β€˜π‘‘) βˆ– I )))) β†’ ((πœ‘ ∧ 𝑒 ∈ dom ((π‘Šβ€˜0) βˆ– I )) β†’ βˆƒπ‘€ ∈ Word 𝑇(((𝐺 Ξ£g 𝑀) = ( I β†Ύ 𝐷) ∧ (β™―β€˜π‘€) = 𝐿) ∧ ((𝑏 + 1) ∈ (0..^𝐿) ∧ 𝑒 ∈ dom ((π‘€β€˜(𝑏 + 1)) βˆ– I ) ∧ βˆ€π‘ ∈ (0..^(𝑏 + 1)) Β¬ 𝑒 ∈ dom ((π‘€β€˜π‘) βˆ– I )))))
151150a1i 11 . . . . . 6 (𝑏 ∈ β„•0 β†’ (((πœ‘ ∧ 𝑒 ∈ dom ((π‘Šβ€˜0) βˆ– I )) β†’ βˆƒπ‘₯ ∈ Word 𝑇(((𝐺 Ξ£g π‘₯) = ( I β†Ύ 𝐷) ∧ (β™―β€˜π‘₯) = 𝐿) ∧ (𝑏 ∈ (0..^𝐿) ∧ 𝑒 ∈ dom ((π‘₯β€˜π‘) βˆ– I ) ∧ βˆ€π‘‘ ∈ (0..^𝑏) Β¬ 𝑒 ∈ dom ((π‘₯β€˜π‘‘) βˆ– I )))) β†’ ((πœ‘ ∧ 𝑒 ∈ dom ((π‘Šβ€˜0) βˆ– I )) β†’ βˆƒπ‘€ ∈ Word 𝑇(((𝐺 Ξ£g 𝑀) = ( I β†Ύ 𝐷) ∧ (β™―β€˜π‘€) = 𝐿) ∧ ((𝑏 + 1) ∈ (0..^𝐿) ∧ 𝑒 ∈ dom ((π‘€β€˜(𝑏 + 1)) βˆ– I ) ∧ βˆ€π‘ ∈ (0..^(𝑏 + 1)) Β¬ 𝑒 ∈ dom ((π‘€β€˜π‘) βˆ– I ))))))
15237, 73, 84, 95, 125, 151nn0ind 12605 . . . . 5 (𝐿 ∈ β„•0 β†’ ((πœ‘ ∧ 𝑒 ∈ dom ((π‘Šβ€˜0) βˆ– I )) β†’ βˆƒπ‘€ ∈ Word 𝑇(((𝐺 Ξ£g 𝑀) = ( I β†Ύ 𝐷) ∧ (β™―β€˜π‘€) = 𝐿) ∧ (𝐿 ∈ (0..^𝐿) ∧ 𝑒 ∈ dom ((π‘€β€˜πΏ) βˆ– I ) ∧ βˆ€π‘ ∈ (0..^𝐿) Β¬ 𝑒 ∈ dom ((π‘€β€˜π‘) βˆ– I )))))
15326, 152mtoi 198 . . . 4 (𝐿 ∈ β„•0 β†’ Β¬ (πœ‘ ∧ 𝑒 ∈ dom ((π‘Šβ€˜0) βˆ– I )))
154153con2i 139 . . 3 ((πœ‘ ∧ 𝑒 ∈ dom ((π‘Šβ€˜0) βˆ– I )) β†’ Β¬ 𝐿 ∈ β„•0)
15521, 154exlimddv 1939 . 2 (πœ‘ β†’ Β¬ 𝐿 ∈ β„•0)
1564, 155pm2.65i 193 1 Β¬ πœ‘
Colors of variables: wff setvar class
Syntax hints:  Β¬ wn 3   β†’ wi 4   ∧ wa 397   ∧ w3a 1088   = wceq 1542  βˆƒwex 1782   ∈ wcel 2107   β‰  wne 2944  βˆ€wral 3065  βˆƒwrex 3074   βˆ– cdif 3912  βˆ…c0 4287   class class class wbr 5110   I cid 5535  dom cdm 5638  ran crn 5639   β†Ύ cres 5640  βŸΆwf 6497  β€˜cfv 6501  (class class class)co 7362  0cc0 11058  1c1 11059   + caddc 11061   < clt 11196   βˆ’ cmin 11392  β„•cn 12160  2c2 12215  β„•0cn0 12420  ..^cfzo 13574  β™―chash 14237  Word cword 14409   Ξ£g cgsu 17329  SymGrpcsymg 19155  pmTrspcpmtr 19230
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2155  ax-12 2172  ax-ext 2708  ax-rep 5247  ax-sep 5261  ax-nul 5268  ax-pow 5325  ax-pr 5389  ax-un 7677  ax-cnex 11114  ax-resscn 11115  ax-1cn 11116  ax-icn 11117  ax-addcl 11118  ax-addrcl 11119  ax-mulcl 11120  ax-mulrcl 11121  ax-mulcom 11122  ax-addass 11123  ax-mulass 11124  ax-distr 11125  ax-i2m1 11126  ax-1ne0 11127  ax-1rid 11128  ax-rnegex 11129  ax-rrecex 11130  ax-cnre 11131  ax-pre-lttri 11132  ax-pre-lttrn 11133  ax-pre-ltadd 11134  ax-pre-mulgt0 11135
This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-3or 1089  df-3an 1090  df-xor 1511  df-tru 1545  df-fal 1555  df-ex 1783  df-nf 1787  df-sb 2069  df-mo 2539  df-eu 2568  df-clab 2715  df-cleq 2729  df-clel 2815  df-nfc 2890  df-ne 2945  df-nel 3051  df-ral 3066  df-rex 3075  df-rmo 3356  df-reu 3357  df-rab 3411  df-v 3450  df-sbc 3745  df-csb 3861  df-dif 3918  df-un 3920  df-in 3922  df-ss 3932  df-pss 3934  df-nul 4288  df-if 4492  df-pw 4567  df-sn 4592  df-pr 4594  df-tp 4596  df-op 4598  df-ot 4600  df-uni 4871  df-int 4913  df-iun 4961  df-br 5111  df-opab 5173  df-mpt 5194  df-tr 5228  df-id 5536  df-eprel 5542  df-po 5550  df-so 5551  df-fr 5593  df-we 5595  df-xp 5644  df-rel 5645  df-cnv 5646  df-co 5647  df-dm 5648  df-rn 5649  df-res 5650  df-ima 5651  df-pred 6258  df-ord 6325  df-on 6326  df-lim 6327  df-suc 6328  df-iota 6453  df-fun 6503  df-fn 6504  df-f 6505  df-f1 6506  df-fo 6507  df-f1o 6508  df-fv 6509  df-riota 7318  df-ov 7365  df-oprab 7366  df-mpo 7367  df-om 7808  df-1st 7926  df-2nd 7927  df-frecs 8217  df-wrecs 8248  df-recs 8322  df-rdg 8361  df-1o 8417  df-2o 8418  df-er 8655  df-map 8774  df-en 8891  df-dom 8892  df-sdom 8893  df-fin 8894  df-card 9882  df-pnf 11198  df-mnf 11199  df-xr 11200  df-ltxr 11201  df-le 11202  df-sub 11394  df-neg 11395  df-nn 12161  df-2 12223  df-3 12224  df-4 12225  df-5 12226  df-6 12227  df-7 12228  df-8 12229  df-9 12230  df-n0 12421  df-xnn0 12493  df-z 12507  df-uz 12771  df-fz 13432  df-fzo 13575  df-seq 13914  df-hash 14238  df-word 14410  df-lsw 14458  df-concat 14466  df-s1 14491  df-substr 14536  df-pfx 14566  df-splice 14645  df-s2 14744  df-struct 17026  df-sets 17043  df-slot 17061  df-ndx 17073  df-base 17091  df-ress 17120  df-plusg 17153  df-tset 17159  df-0g 17330  df-gsum 17331  df-mgm 18504  df-sgrp 18553  df-mnd 18564  df-submnd 18609  df-efmnd 18686  df-grp 18758  df-minusg 18759  df-subg 18932  df-symg 19156  df-pmtr 19231
This theorem is referenced by:  psgnunilem4  19286
  Copyright terms: Public domain W3C validator